updated files to recent changes

--- a/doc-src/TutorialI/Datatype/Nested.thy	Thu Sep 30 08:50:45 2010 +0200
+++ b/doc-src/TutorialI/Datatype/Nested.thy	Thu Sep 30 09:31:07 2010 +0200
@@ -111,14 +111,13 @@
 
 (* Exercise 2: *)
 
-consts trev :: "('v,'f) term \<Rightarrow> ('v,'f) term"
-       trevs:: "('v,'f) term list \<Rightarrow> ('v,'f) term list"
-primrec
-"trev (Var v)    = Var v"
-"trev (App f ts) = App f (trevs ts)"
-
-"trevs [] = []"
-"trevs (t#ts) = (trevs ts) @ [(trev t)]" 
+primrec trev :: "('v,'f) term \<Rightarrow> ('v,'f) term"
+  and trevs:: "('v,'f) term list \<Rightarrow> ('v,'f) term list"
+where
+  "trev (Var v)    = Var v"
+| "trev (App f ts) = App f (trevs ts)"
+| "trevs [] = []"
+| "trevs (t#ts) = (trevs ts) @ [(trev t)]" 
 
 lemma [simp]: "\<forall> ys. trevs (xs @ ys) = (trevs ys) @ (trevs xs)" 
 apply (induct_tac xs, auto)

--- a/doc-src/TutorialI/Inductive/Advanced.thy	Thu Sep 30 08:50:45 2010 +0200
+++ b/doc-src/TutorialI/Inductive/Advanced.thy	Thu Sep 30 09:31:07 2010 +0200
@@ -1,4 +1,3 @@
-(* ID:         $Id$ *)
 (*<*)theory Advanced imports Even uses "../../antiquote_setup.ML" begin(*>*)
 
 text {*
@@ -360,11 +359,12 @@
 (*<*)
 
 text{*the following declaration isn't actually used*}
-consts integer_arity :: "integer_op \<Rightarrow> nat"
 primrec
-"integer_arity (Number n)        = 0"
-"integer_arity UnaryMinus        = 1"
-"integer_arity Plus              = 2"
+  integer_arity :: "integer_op \<Rightarrow> nat"
+where
+  "integer_arity (Number n)        = 0"
+| "integer_arity UnaryMinus        = 1"
+| "integer_arity Plus              = 2"
 
 text{* the rest isn't used: too complicated.  OK for an exercise though.*}
 

--- a/doc-src/TutorialI/Protocol/Event.thy	Thu Sep 30 08:50:45 2010 +0200
+++ b/doc-src/TutorialI/Protocol/Event.thy	Thu Sep 30 09:31:07 2010 +0200
@@ -23,24 +23,15 @@
        
 consts 
   bad    :: "agent set"                         -- {* compromised agents *}
-  knows  :: "agent => event list => msg set"
 
 
 text{*The constant "spies" is retained for compatibility's sake*}
 
-abbreviation (input)
-  spies  :: "event list => msg set" where
-  "spies == knows Spy"
-
-text{*Spy has access to his own key for spoof messages, but Server is secure*}
-specification (bad)
-  Spy_in_bad     [iff]: "Spy \<in> bad"
-  Server_not_bad [iff]: "Server \<notin> bad"
-    by (rule exI [of _ "{Spy}"], simp)
-
 primrec
+  knows :: "agent => event list => msg set"
+where
   knows_Nil:   "knows A [] = initState A"
-  knows_Cons:
+| knows_Cons:
     "knows A (ev # evs) =
        (if A = Spy then 
         (case ev of
@@ -57,20 +48,29 @@
          | Notes A' X    => 
              if A'=A then insert X (knows A evs) else knows A evs))"
 
+abbreviation (input)
+  spies  :: "event list => msg set" where
+  "spies == knows Spy"
+
+text{*Spy has access to his own key for spoof messages, but Server is secure*}
+specification (bad)
+  Spy_in_bad     [iff]: "Spy \<in> bad"
+  Server_not_bad [iff]: "Server \<notin> bad"
+    by (rule exI [of _ "{Spy}"], simp)
+
 (*
   Case A=Spy on the Gets event
   enforces the fact that if a message is received then it must have been sent,
   therefore the oops case must use Notes
 *)
 
-consts
+primrec
   (*Set of items that might be visible to somebody:
     complement of the set of fresh items*)
   used :: "event list => msg set"
-
-primrec
+where
   used_Nil:   "used []         = (UN B. parts (initState B))"
-  used_Cons:  "used (ev # evs) =
+| used_Cons:  "used (ev # evs) =
                      (case ev of
                         Says A B X => parts {X} \<union> used evs
                       | Gets A X   => used evs

--- a/doc-src/TutorialI/Protocol/Public.thy	Thu Sep 30 08:50:45 2010 +0200
+++ b/doc-src/TutorialI/Protocol/Public.thy	Thu Sep 30 09:31:07 2010 +0200
@@ -22,14 +22,19 @@
 abbreviation priK :: "agent \<Rightarrow> key"
 where "priK x  \<equiv>  invKey(pubK x)"
 (*<*)
-primrec
+overloading initState \<equiv> initState
+begin
+
+primrec initState where
         (*Agents know their private key and all public keys*)
   initState_Server:  "initState Server     =    
                          insert (Key (priK Server)) (Key ` range pubK)"
-  initState_Friend:  "initState (Friend i) =    
+| initState_Friend:  "initState (Friend i) =    
                          insert (Key (priK (Friend i))) (Key ` range pubK)"
-  initState_Spy:     "initState Spy        =    
+| initState_Spy:     "initState Spy        =    
                          (Key`invKey`pubK`bad) Un (Key ` range pubK)"
+
+end
 (*>*)
 
 text {*

--- a/doc-src/TutorialI/Sets/Examples.thy	Thu Sep 30 08:50:45 2010 +0200
+++ b/doc-src/TutorialI/Sets/Examples.thy	Thu Sep 30 09:31:07 2010 +0200
@@ -95,8 +95,8 @@
 text{*
 set extensionality
 
-@{thm[display] set_ext[no_vars]}
-\rulename{set_ext}
+@{thm[display] set_eqI[no_vars]}
+\rulename{set_eqI}
 
 @{thm[display] equalityI[no_vars]}
 \rulename{equalityI}

--- a/doc-src/TutorialI/Sets/Functions.thy	Thu Sep 30 08:50:45 2010 +0200
+++ b/doc-src/TutorialI/Sets/Functions.thy	Thu Sep 30 09:31:07 2010 +0200
@@ -66,20 +66,18 @@
 \rulename{o_inv_distrib}
 *}
 
-
-
 text{*
 small sample proof
 
 @{thm[display] ext[no_vars]}
 \rulename{ext}
 
-@{thm[display] expand_fun_eq[no_vars]}
-\rulename{expand_fun_eq}
+@{thm[display] fun_eq_iff[no_vars]}
+\rulename{fun_eq_iff}
 *}
 
 lemma "inj f \<Longrightarrow> (f o g = f o h) = (g = h)";
-  apply (simp add: expand_fun_eq inj_on_def)
+  apply (simp add: fun_eq_iff inj_on_def)
   apply (auto)
   done