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.
ML adaptions
authorhaftmann
Tue, 08 May 2007 08:21:39 +0200
changeset 22862 3dd306cb98d2
parent 22861 8ec47039614e
child 22863 e1d3fa78b8e1
ML adaptions
doc-src/TutorialI/Protocol/Message_lemmas.ML file | annotate | diff | comparison | revisions
doc-src/TutorialI/Protocol/Public_lemmas.ML file | annotate | diff | comparison | revisions 
--- a/doc-src/TutorialI/Protocol/Message_lemmas.ML	Tue May 08 05:30:10 2007 +0200
+++ b/doc-src/TutorialI/Protocol/Message_lemmas.ML	Tue May 08 08:21:39 2007 +0200
@@ -849,7 +849,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;
 
 fun Fake_parts_insert_tac i = 
--- a/doc-src/TutorialI/Protocol/Public_lemmas.ML	Tue May 08 05:30:10 2007 +0200
+++ b/doc-src/TutorialI/Protocol/Public_lemmas.ML	Tue May 08 08:21:39 2007 +0200
@@ -13,7 +13,7 @@
 
 (*** Basic properties of pubK & priK ***)
 
-AddIffs [inj_pubK RS inj_eq];
+AddIffs [inj_pubK RS @{thm inj_eq}];
 
 Goal "(priK A = priK B) = (A=B)";
 by Safe_tac;
isabelle