diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /test-suite/ide/undo014.fake | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/ide/undo014.fake')
-rw-r--r-- | test-suite/ide/undo014.fake | 36 |
1 files changed, 18 insertions, 18 deletions
diff --git a/test-suite/ide/undo014.fake b/test-suite/ide/undo014.fake index 5224b504..6d58b061 100644 --- a/test-suite/ide/undo014.fake +++ b/test-suite/ide/undo014.fake @@ -4,23 +4,23 @@ # Test backtracking in presence of nested proofs # Third, undo inside an inner proof # -INTERP Lemma aa : True -> True /\ True. -INTERP intro H. -INTERP split. -INTERP Lemma bb : False -> False. -INTERP intro H. -INTERP apply H. -INTERP Qed. -INTERP apply H. -INTERP Lemma cc : False -> True. -INTERP intro H. -INTERP destruct H. -REWIND 1 +ADD { Lemma aa : True -> True /\ True. } +ADD { intro H. } +ADD { split. } +ADD { Lemma bb : False -> False. } +ADD { intro H. } +ADD { apply H. } +ADD { Qed. } +ADD { apply H. } +ADD { Lemma cc : False -> True. } +ADD here { intro H. } +ADD { destruct H. } +EDIT_AT here # <replay> -INTERP destruct H. +ADD { destruct H. } # </replay> -INTERP Qed. -INTERP apply H. -INTERP Qed. -INTERPRAW Fail idtac. -INTERPRAW Check (aa,bb,cc). +ADD { Qed. } +ADD { apply H. } +ADD { Qed. } +QUERY { Fail idtac. } +QUERY { Check (aa,bb,cc). } |