diff options
Diffstat (limited to 'test-suite/ide/undo009.fake')
-rw-r--r-- | test-suite/ide/undo009.fake | 25 |
1 files changed, 13 insertions, 12 deletions
diff --git a/test-suite/ide/undo009.fake b/test-suite/ide/undo009.fake index 47c77d23..76f400ef 100644 --- a/test-suite/ide/undo009.fake +++ b/test-suite/ide/undo009.fake @@ -4,17 +4,18 @@ # Undoing declarations, interleaved with proof steps # new in 8.2 *) # -INTERP Theorem k : O=O. -INTERP assert True by trivial. -INTERP Definition l := O. -INTERP assert True by trivial. -INTERP Definition m := O. -REWIND 3 +ADD { Theorem k : O=O. } +ADD here { assert True by trivial. } +ADD { Definition l := O. } +ADD { assert True by trivial. } +ADD { Definition m := O. } +QUERY { Show. } +EDIT_AT here # <replay> -INTERP Definition l := O. -INTERP assert True by trivial. -INTERP Definition m := O. +ADD { Definition l := O. } +ADD { assert True by trivial. } +ADD { Definition m := O. } # <\replay> -INTERP assert True by trivial. -INTERP trivial. -INTERP Qed. +ADD { assert True by trivial. } +ADD { trivial. } +ADD { Qed. } |