# HG changeset patch
# User wenzelm
# Date 1284126523 -7200
# Node ID 7c69964c6d741e235f1dde20008fc36cf9d598aa
# Parent  148b78fb70d827975bd32b6d0cbda425d76e3edf
proper antiquotations;

diff -r 148b78fb70d8 -r 7c69964c6d74 doc-src/TutorialI/Protocol/Event.thy
--- a/doc-src/TutorialI/Protocol/Event.thy	Fri Sep 10 15:42:14 2010 +0200
+++ b/doc-src/TutorialI/Protocol/Event.thy	Fri Sep 10 15:48:43 2010 +0200
@@ -296,40 +296,40 @@
 
 ML
 {*
-val knows_Cons     = thm "knows_Cons"
-val used_Nil       = thm "used_Nil"
-val used_Cons      = thm "used_Cons"
+val knows_Cons = @{thm knows_Cons};
+val used_Nil = @{thm used_Nil};
+val used_Cons = @{thm used_Cons};
 
-val Notes_imp_used = thm "Notes_imp_used";
-val Says_imp_used = thm "Says_imp_used";
-val Says_imp_knows_Spy = thm "Says_imp_knows_Spy";
-val Notes_imp_knows_Spy = thm "Notes_imp_knows_Spy";
-val knows_Spy_partsEs = thms "knows_Spy_partsEs";
-val spies_partsEs = thms "spies_partsEs";
-val Says_imp_spies = thm "Says_imp_spies";
-val parts_insert_spies = thm "parts_insert_spies";
-val Says_imp_knows = thm "Says_imp_knows";
-val Notes_imp_knows = thm "Notes_imp_knows";
-val Gets_imp_knows_agents = thm "Gets_imp_knows_agents";
-val knows_imp_Says_Gets_Notes_initState = thm "knows_imp_Says_Gets_Notes_initState";
-val knows_Spy_imp_Says_Notes_initState = thm "knows_Spy_imp_Says_Notes_initState";
-val usedI = thm "usedI";
-val initState_into_used = thm "initState_into_used";
-val used_Says = thm "used_Says";
-val used_Notes = thm "used_Notes";
-val used_Gets = thm "used_Gets";
-val used_nil_subset = thm "used_nil_subset";
-val analz_mono_contra = thms "analz_mono_contra";
-val knows_subset_knows_Cons = thm "knows_subset_knows_Cons";
-val initState_subset_knows = thm "initState_subset_knows";
-val keysFor_parts_insert = thm "keysFor_parts_insert";
+val Notes_imp_used = @{thm Notes_imp_used};
+val Says_imp_used = @{thm Says_imp_used};
+val Says_imp_knows_Spy = @{thm Says_imp_knows_Spy};
+val Notes_imp_knows_Spy = @{thm Notes_imp_knows_Spy};
+val knows_Spy_partsEs = @{thms knows_Spy_partsEs};
+val spies_partsEs = @{thms spies_partsEs};
+val Says_imp_spies = @{thm Says_imp_spies};
+val parts_insert_spies = @{thm parts_insert_spies};
+val Says_imp_knows = @{thm Says_imp_knows};
+val Notes_imp_knows = @{thm Notes_imp_knows};
+val Gets_imp_knows_agents = @{thm Gets_imp_knows_agents};
+val knows_imp_Says_Gets_Notes_initState = @{thm knows_imp_Says_Gets_Notes_initState};
+val knows_Spy_imp_Says_Notes_initState = @{thm knows_Spy_imp_Says_Notes_initState};
+val usedI = @{thm usedI};
+val initState_into_used = @{thm initState_into_used};
+val used_Says = @{thm used_Says};
+val used_Notes = @{thm used_Notes};
+val used_Gets = @{thm used_Gets};
+val used_nil_subset = @{thm used_nil_subset};
+val analz_mono_contra = @{thms analz_mono_contra};
+val knows_subset_knows_Cons = @{thm knows_subset_knows_Cons};
+val initState_subset_knows = @{thm initState_subset_knows};
+val keysFor_parts_insert = @{thm keysFor_parts_insert};
 
 
-val synth_analz_mono = thm "synth_analz_mono";
+val synth_analz_mono = @{thm synth_analz_mono};
 
-val knows_Spy_subset_knows_Spy_Says = thm "knows_Spy_subset_knows_Spy_Says";
-val knows_Spy_subset_knows_Spy_Notes = thm "knows_Spy_subset_knows_Spy_Notes";
-val knows_Spy_subset_knows_Spy_Gets = thm "knows_Spy_subset_knows_Spy_Gets";
+val knows_Spy_subset_knows_Spy_Says = @{thm knows_Spy_subset_knows_Spy_Says};
+val knows_Spy_subset_knows_Spy_Notes = @{thm knows_Spy_subset_knows_Spy_Notes};
+val knows_Spy_subset_knows_Spy_Gets = @{thm knows_Spy_subset_knows_Spy_Gets};
 
 
 val synth_analz_mono_contra_tac = 
diff -r 148b78fb70d8 -r 7c69964c6d74 doc-src/TutorialI/Protocol/Message.thy
--- a/doc-src/TutorialI/Protocol/Message.thy	Fri Sep 10 15:42:14 2010 +0200
+++ b/doc-src/TutorialI/Protocol/Message.thy	Fri Sep 10 15:48:43 2010 +0200
@@ -809,19 +809,19 @@
 subsection{*Tactics useful for many protocol proofs*}
 ML
 {*
-val invKey = thm "invKey"
-val keysFor_def = thm "keysFor_def"
-val symKeys_def = thm "symKeys_def"
-val parts_mono = thm "parts_mono";
-val analz_mono = thm "analz_mono";
-val synth_mono = thm "synth_mono";
-val analz_increasing = thm "analz_increasing";
+val invKey = @{thm invKey};
+val keysFor_def = @{thm keysFor_def};
+val symKeys_def = @{thm symKeys_def};
+val parts_mono = @{thm parts_mono};
+val analz_mono = @{thm analz_mono};
+val synth_mono = @{thm synth_mono};
+val analz_increasing = @{thm analz_increasing};
 
-val analz_insertI = thm "analz_insertI";
-val analz_subset_parts = thm "analz_subset_parts";
-val Fake_parts_insert = thm "Fake_parts_insert";
-val Fake_analz_insert = thm "Fake_analz_insert";
-val pushes = thms "pushes";
+val analz_insertI = @{thm analz_insertI};
+val analz_subset_parts = @{thm analz_subset_parts};
+val Fake_parts_insert = @{thm Fake_parts_insert};
+val Fake_analz_insert = @{thm Fake_analz_insert};
+val pushes = @{thms pushes};
 
 
 (*Prove base case (subgoal i) and simplify others.  A typical base case
@@ -844,7 +844,7 @@
 val Fake_insert_tac = 
     dresolve_tac [impOfSubs Fake_analz_insert,
                   impOfSubs Fake_parts_insert] THEN'
-    eresolve_tac [asm_rl, thm"synth.Inj"];
+    eresolve_tac [asm_rl, @{thm synth.Inj}];
 
 fun Fake_insert_simp_tac ss i = 
     REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;