--- a/Quot/Examples/Larry.thy	Thu Dec 10 18:28:41 2009 +0100
+++ b/Quot/Examples/Larry.thy	Thu Dec 10 19:05:56 2009 +0100
@@ -22,6 +22,8 @@
 | SYM:   "X \<sim> Y \<Longrightarrow> Y \<sim> X"
 | TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"
 
+lemmas msgrel.intros[intro]
+
 text{*Proving that it is an equivalence relation*}
 
 lemma msgrel_refl: "X \<sim> X"
@@ -38,7 +40,7 @@
 
 subsubsection{*The Set of Nonces*}
 
-primrec
+fun
   freenonces :: "freemsg \<Rightarrow> nat set"
 where
   "freenonces (NONCE N) = {N}"
@@ -47,8 +49,9 @@
 | "freenonces (DECRYPT K X) = freenonces X"
 
 theorem msgrel_imp_eq_freenonces: 
-  "U \<sim> V \<Longrightarrow> freenonces U = freenonces V"
-by (erule msgrel.induct, auto) 
+  assumes a: "U \<sim> V"
+  shows "freenonces U = freenonces V"
+using a by (induct) (auto) 
 
 subsubsection{*The Left Projection*}
 
@@ -67,15 +70,13 @@
   (the abstract constructor) is injective*}
 lemma msgrel_imp_eqv_freeleft_aux:
   shows "freeleft U \<sim> freeleft U"
-apply(induct rule: freeleft.induct)
-apply(auto intro: msgrel.intros)
-done
+by (induct rule: freeleft.induct) (auto)
 
 theorem msgrel_imp_eqv_freeleft:
-  "U \<sim> V \<Longrightarrow> freeleft U \<sim> freeleft V"
-apply(erule msgrel.induct)
-apply(auto intro: msgrel.intros msgrel_imp_eqv_freeleft_aux)
-done
+  assumes a: "U \<sim> V" 
+  shows "freeleft U \<sim> freeleft V"
+using a
+by (induct)(auto intro: msgrel_imp_eqv_freeleft_aux)
 
 subsubsection{*The Right Projection*}
 
@@ -93,13 +94,13 @@
   (the abstract constructor) is injective*}
 lemma msgrel_imp_eqv_freeright_aux:
   shows "freeright U \<sim> freeright U"
-apply(induct rule: freeright.induct)
-apply(auto intro: msgrel.intros)
-done
+by (induct rule: freeright.induct) (auto)
 
 theorem msgrel_imp_eqv_freeright:
-     "U \<sim> V \<Longrightarrow> freeright U \<sim> freeright V"
-by (erule msgrel.induct, auto intro: msgrel.intros msgrel_imp_eqv_freeright_aux)
+  assumes a: "U \<sim> V" 
+  shows "freeright U \<sim> freeright V"
+using a
+by (induct) (auto intro: msgrel_imp_eqv_freeright_aux)
 
 subsubsection{*The Discriminator for Constructors*}
 
@@ -114,8 +115,9 @@
 
 text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}
 theorem msgrel_imp_eq_freediscrim:
-     "U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V"
-by (erule msgrel.induct, auto)
+  assumes a: "U \<sim> V"
+  shows "freediscrim U = freediscrim V"
+using a by (induct, auto)
 
 
 subsection{*The Initial Algebra: A Quotiented Message Type*}
@@ -261,14 +263,17 @@
 text{*Can also be proved using the function @{term nonces}*}
 lemma Nonce_Nonce_eq [iff]: 
   shows "(Nonce m = Nonce n) = (m = n)"
-apply(rule iffI)
-apply(lifting NONCE_imp_eq)
-apply(simp)
-done
+proof
+  assume "Nonce m = Nonce n"
+  then show "m = n" by (lifting NONCE_imp_eq)
+next
+  assume "m = n" 
+  then show "Nonce m = Nonce n" by simp
+qed
 
 lemma MPAIR_imp_eqv_left: 
   shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
-by (drule msgrel_imp_eqv_freeleft, simp)
+by (drule msgrel_imp_eqv_freeleft) (simp)
 
 lemma MPair_imp_eq_left: 
   assumes eq: "MPair X Y = MPair X' Y'" 
@@ -277,7 +282,7 @@
 
 lemma MPAIR_imp_eqv_right: 
   shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
-by (drule msgrel_imp_eqv_freeright, simp)
+by (drule msgrel_imp_eqv_freeright) (simp)
 
 lemma MPair_imp_eq_right: 
   shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"