• Andrei Paskevich's avatar
    Introduction: "generalize_introduced" moves local premises back to the goal · e3cfcd52
    Andrei Paskevich authored
    See #151.
    At the moment, this transformation is only integrated into TryWhy3,
    in order to restore left-hand side splitting under vc:sp.
    
    I suggest to integrate "generalize" into split_vc unconditionally.
    I've tested that, the sessions were only broken for 4 examples:
      examples/tortoise_and_hare/
      examples/verifythis_2018_array_based_queuing_lock_2/
      examples/verifythis_2018_mind_the_gap_2/
      examples/multiprecision/toom/
    e3cfcd52
introduction.ml 9.26 KB