Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
OldGoals.inst;
authorwenzelm
Wed, 11 Jun 2008 18:15:36 +0200
changeset 27159 9506c7e73cfa
parent 27158 113a32dd0b14
child 27160 1ef88d06362f
OldGoals.inst;
src/HOL/SET-Protocol/EventSET.thy file | annotate | diff | comparison | revisions
src/HOL/SET-Protocol/MessageSET.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/SET-Protocol/EventSET.thy	Wed Jun 11 18:04:02 2008 +0200
+++ b/src/HOL/SET-Protocol/EventSET.thy	Wed Jun 11 18:15:36 2008 +0200
@@ -180,7 +180,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 (dresolve_tac @{thms analz_mono_contra}) THEN'
      mp_tac
--- a/src/HOL/SET-Protocol/MessageSET.thy	Wed Jun 11 18:04:02 2008 +0200
+++ b/src/HOL/SET-Protocol/MessageSET.thy	Wed Jun 11 18:15:36 2008 +0200
@@ -815,7 +815,7 @@
     be pulled out using the @{text analz_insert} rules*}
 ML
 {*
-fun insComm x y = inst "x" x (inst "y" y insert_commute);
+fun insComm x y = OldGoals.inst "x" x (OldGoals.inst "y" y insert_commute);
 
 bind_thms ("pushKeys",
            map (insComm "Key ?K")
isabelle