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.
dropped legacy ML binding
authorhaftmann
Sun, 06 May 2007 21:49:32 +0200
changeset 22843 189e214845dd
parent 22842 6d2fd4e0f984
child 22844 91c05f4b509e
dropped legacy ML binding
src/HOL/Auth/Message.thy file | annotate | diff | comparison | revisions
src/HOL/SET-Protocol/MessageSET.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Auth/Message.thy	Sun May 06 21:49:29 2007 +0200
+++ b/src/HOL/Auth/Message.thy	Sun May 06 21:49:32 2007 +0200
@@ -857,7 +857,7 @@
   concerns  Crypt K X \<notin> Key`shrK`bad  and cannot be proved by rewriting
   alone.*)
 fun prove_simple_subgoals_tac i = 
-    force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN
+    force_tac (claset(), simpset() addsimps [@{thm image_eq_UN}]) i THEN
     ALLGOALS Asm_simp_tac
 
 (*Analysis of Fake cases.  Also works for messages that forward unknown parts,
--- a/src/HOL/SET-Protocol/MessageSET.thy	Sun May 06 21:49:29 2007 +0200
+++ b/src/HOL/SET-Protocol/MessageSET.thy	Sun May 06 21:49:32 2007 +0200
@@ -844,7 +844,7 @@
   concerns  Crypt K X \<notin> Key`shrK`bad  and cannot be proved by rewriting
   alone.*)
 fun prove_simple_subgoals_tac i =
-    force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN
+    force_tac (claset(), simpset() addsimps [@{thm image_eq_UN}]) i THEN
     ALLGOALS Asm_simp_tac
 
 (*Analysis of Fake cases.  Also works for messages that forward unknown parts,
isabelle