diff -r 0fd4abb5fade -r f51c6069cd17 Quot/Examples/Larry.thy
--- a/Quot/Examples/Larry.thy	Fri Dec 11 08:28:41 2009 +0100
+++ b/Quot/Examples/Larry.thy	Fri Dec 11 11:08:58 2009 +0100
@@ -128,23 +128,23 @@
 text{*The abstract message constructors*}
 
 quotient_def
-  Nonce::"Nonce :: nat \<Rightarrow> msg"
-where
+  "Nonce :: nat \<Rightarrow> msg"
+as
   "NONCE"
 
 quotient_def
-  MPair::"MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
-where
+  "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
+as
   "MPAIR"
 
 quotient_def
-  Crypt::"Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
-where
+  "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
+as
   "CRYPT"
 
 quotient_def
-  Decrypt::"Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
-where
+  "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
+as
   "DECRYPT"
 
 lemma [quot_respect]:
@@ -165,8 +165,8 @@
 subsection{*The Abstract Function to Return the Set of Nonces*}
 
 quotient_def
-  nonces :: "nounces:: msg \<Rightarrow> nat set"
-where
+   "nonces:: msg \<Rightarrow> nat set"
+as
   "freenonces"
 
 text{*Now prove the four equations for @{term nonces}*}
@@ -201,8 +201,8 @@
 subsection{*The Abstract Function to Return the Left Part*}
 
 quotient_def
-  left :: "left:: msg \<Rightarrow> msg"
-where
+  "left:: msg \<Rightarrow> msg"
+as
   "freeleft"
 
 lemma [quot_respect]:
@@ -228,8 +228,8 @@
 subsection{*The Abstract Function to Return the Right Part*}
 
 quotient_def
-  right :: "right:: msg \<Rightarrow> msg"
-where
+  "right:: msg \<Rightarrow> msg"
+as
   "freeright"
 
 text{*Now prove the four equations for @{term right}*}
@@ -362,8 +362,8 @@
 need this function in order to prove discrimination theorems.*}
 
 quotient_def
-  discrim :: "discrim:: msg \<Rightarrow> int"
-where
+  "discrim:: msg \<Rightarrow> int"
+as
   "freediscrim"
 
 text{*Now prove the four equations for @{term discrim}*}