1.1 --- a/doc-src/TutorialI/Protocol/Event.thy	Fri Sep 10 15:42:14 2010 +0200
     1.2 +++ b/doc-src/TutorialI/Protocol/Event.thy	Fri Sep 10 15:48:43 2010 +0200
     1.3 @@ -296,40 +296,40 @@
     1.4  
     1.5  ML
     1.6  {*
     1.7 -val knows_Cons     = thm "knows_Cons"
     1.8 -val used_Nil       = thm "used_Nil"
     1.9 -val used_Cons      = thm "used_Cons"
    1.10 +val knows_Cons = @{thm knows_Cons};
    1.11 +val used_Nil = @{thm used_Nil};
    1.12 +val used_Cons = @{thm used_Cons};
    1.13  
    1.14 -val Notes_imp_used = thm "Notes_imp_used";
    1.15 -val Says_imp_used = thm "Says_imp_used";
    1.16 -val Says_imp_knows_Spy = thm "Says_imp_knows_Spy";
    1.17 -val Notes_imp_knows_Spy = thm "Notes_imp_knows_Spy";
    1.18 -val knows_Spy_partsEs = thms "knows_Spy_partsEs";
    1.19 -val spies_partsEs = thms "spies_partsEs";
    1.20 -val Says_imp_spies = thm "Says_imp_spies";
    1.21 -val parts_insert_spies = thm "parts_insert_spies";
    1.22 -val Says_imp_knows = thm "Says_imp_knows";
    1.23 -val Notes_imp_knows = thm "Notes_imp_knows";
    1.24 -val Gets_imp_knows_agents = thm "Gets_imp_knows_agents";
    1.25 -val knows_imp_Says_Gets_Notes_initState = thm "knows_imp_Says_Gets_Notes_initState";
    1.26 -val knows_Spy_imp_Says_Notes_initState = thm "knows_Spy_imp_Says_Notes_initState";
    1.27 -val usedI = thm "usedI";
    1.28 -val initState_into_used = thm "initState_into_used";
    1.29 -val used_Says = thm "used_Says";
    1.30 -val used_Notes = thm "used_Notes";
    1.31 -val used_Gets = thm "used_Gets";
    1.32 -val used_nil_subset = thm "used_nil_subset";
    1.33 -val analz_mono_contra = thms "analz_mono_contra";
    1.34 -val knows_subset_knows_Cons = thm "knows_subset_knows_Cons";
    1.35 -val initState_subset_knows = thm "initState_subset_knows";
    1.36 -val keysFor_parts_insert = thm "keysFor_parts_insert";
    1.37 +val Notes_imp_used = @{thm Notes_imp_used};
    1.38 +val Says_imp_used = @{thm Says_imp_used};
    1.39 +val Says_imp_knows_Spy = @{thm Says_imp_knows_Spy};
    1.40 +val Notes_imp_knows_Spy = @{thm Notes_imp_knows_Spy};
    1.41 +val knows_Spy_partsEs = @{thms knows_Spy_partsEs};
    1.42 +val spies_partsEs = @{thms spies_partsEs};
    1.43 +val Says_imp_spies = @{thm Says_imp_spies};
    1.44 +val parts_insert_spies = @{thm parts_insert_spies};
    1.45 +val Says_imp_knows = @{thm Says_imp_knows};
    1.46 +val Notes_imp_knows = @{thm Notes_imp_knows};
    1.47 +val Gets_imp_knows_agents = @{thm Gets_imp_knows_agents};
    1.48 +val knows_imp_Says_Gets_Notes_initState = @{thm knows_imp_Says_Gets_Notes_initState};
    1.49 +val knows_Spy_imp_Says_Notes_initState = @{thm knows_Spy_imp_Says_Notes_initState};
    1.50 +val usedI = @{thm usedI};
    1.51 +val initState_into_used = @{thm initState_into_used};
    1.52 +val used_Says = @{thm used_Says};
    1.53 +val used_Notes = @{thm used_Notes};
    1.54 +val used_Gets = @{thm used_Gets};
    1.55 +val used_nil_subset = @{thm used_nil_subset};
    1.56 +val analz_mono_contra = @{thms analz_mono_contra};
    1.57 +val knows_subset_knows_Cons = @{thm knows_subset_knows_Cons};
    1.58 +val initState_subset_knows = @{thm initState_subset_knows};
    1.59 +val keysFor_parts_insert = @{thm keysFor_parts_insert};
    1.60  
    1.61  
    1.62 -val synth_analz_mono = thm "synth_analz_mono";
    1.63 +val synth_analz_mono = @{thm synth_analz_mono};
    1.64  
    1.65 -val knows_Spy_subset_knows_Spy_Says = thm "knows_Spy_subset_knows_Spy_Says";
    1.66 -val knows_Spy_subset_knows_Spy_Notes = thm "knows_Spy_subset_knows_Spy_Notes";
    1.67 -val knows_Spy_subset_knows_Spy_Gets = thm "knows_Spy_subset_knows_Spy_Gets";
    1.68 +val knows_Spy_subset_knows_Spy_Says = @{thm knows_Spy_subset_knows_Spy_Says};
    1.69 +val knows_Spy_subset_knows_Spy_Notes = @{thm knows_Spy_subset_knows_Spy_Notes};
    1.70 +val knows_Spy_subset_knows_Spy_Gets = @{thm knows_Spy_subset_knows_Spy_Gets};
    1.71  
    1.72  
    1.73  val synth_analz_mono_contra_tac = 

     2.1 --- a/doc-src/TutorialI/Protocol/Message.thy	Fri Sep 10 15:42:14 2010 +0200
     2.2 +++ b/doc-src/TutorialI/Protocol/Message.thy	Fri Sep 10 15:48:43 2010 +0200
     2.3 @@ -809,19 +809,19 @@
     2.4  subsection{*Tactics useful for many protocol proofs*}
     2.5  ML
     2.6  {*
     2.7 -val invKey = thm "invKey"
     2.8 -val keysFor_def = thm "keysFor_def"
     2.9 -val symKeys_def = thm "symKeys_def"
    2.10 -val parts_mono = thm "parts_mono";
    2.11 -val analz_mono = thm "analz_mono";
    2.12 -val synth_mono = thm "synth_mono";
    2.13 -val analz_increasing = thm "analz_increasing";
    2.14 +val invKey = @{thm invKey};
    2.15 +val keysFor_def = @{thm keysFor_def};
    2.16 +val symKeys_def = @{thm symKeys_def};
    2.17 +val parts_mono = @{thm parts_mono};
    2.18 +val analz_mono = @{thm analz_mono};
    2.19 +val synth_mono = @{thm synth_mono};
    2.20 +val analz_increasing = @{thm analz_increasing};
    2.21  
    2.22 -val analz_insertI = thm "analz_insertI";
    2.23 -val analz_subset_parts = thm "analz_subset_parts";
    2.24 -val Fake_parts_insert = thm "Fake_parts_insert";
    2.25 -val Fake_analz_insert = thm "Fake_analz_insert";
    2.26 -val pushes = thms "pushes";
    2.27 +val analz_insertI = @{thm analz_insertI};
    2.28 +val analz_subset_parts = @{thm analz_subset_parts};
    2.29 +val Fake_parts_insert = @{thm Fake_parts_insert};
    2.30 +val Fake_analz_insert = @{thm Fake_analz_insert};
    2.31 +val pushes = @{thms pushes};
    2.32  
    2.33  
    2.34  (*Prove base case (subgoal i) and simplify others.  A typical base case
    2.35 @@ -844,7 +844,7 @@
    2.36  val Fake_insert_tac = 
    2.37      dresolve_tac [impOfSubs Fake_analz_insert,
    2.38                    impOfSubs Fake_parts_insert] THEN'
    2.39 -    eresolve_tac [asm_rl, thm"synth.Inj"];
    2.40 +    eresolve_tac [asm_rl, @{thm synth.Inj}];
    2.41  
    2.42  fun Fake_insert_simp_tac ss i = 
    2.43      REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;