Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/TutorialI/Protocol/Event.thy
changeset 27154 026f3db3f5c6
parent 23925 ee98c2528a8f
child 27225 b316dde851f5 
--- a/doc-src/TutorialI/Protocol/Event.thy	Wed Jun 11 18:02:00 2008 +0200
+++ b/doc-src/TutorialI/Protocol/Event.thy	Wed Jun 11 18:02:25 2008 +0200
@@ -261,7 +261,7 @@
 ML
 {*
 val analz_mono_contra_tac = 
-  let val analz_impI = inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
+  let val analz_impI = OldGoals.inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
   in
     rtac analz_impI THEN' 
     REPEAT1 o 
@@ -334,7 +334,7 @@
 
 
 val synth_analz_mono_contra_tac = 
-  let val syan_impI = inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
+  let val syan_impI = OldGoals.inst "P" "?Y \<notin> synth (analz (knows Spy ?evs))" impI
   in
     rtac syan_impI THEN' 
     REPEAT1 o
isabelle