diff -r 93c9022ba5e9 -r c4001cda9da3 Quot/Examples/LarryDatatype.thy
--- a/Quot/Examples/LarryDatatype.thy	Fri Feb 12 15:50:43 2010 +0100
+++ b/Quot/Examples/LarryDatatype.thy	Fri Feb 12 16:04:10 2010 +0100
@@ -128,22 +128,22 @@
 
 quotient_definition
   "Nonce :: nat \<Rightarrow> msg"
-as
+is
   "NONCE"
 
 quotient_definition
   "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
-as
+is
   "MPAIR"
 
 quotient_definition
   "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
-as
+is
   "CRYPT"
 
 quotient_definition
   "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
-as
+is
   "DECRYPT"
 
 lemma [quot_respect]:
@@ -167,7 +167,7 @@
 
 quotient_definition
    "nonces:: msg \<Rightarrow> nat set"
-as
+is
   "freenonces"
 
 text{*Now prove the four equations for @{term nonces}*}
@@ -204,7 +204,7 @@
 
 quotient_definition
   "left:: msg \<Rightarrow> msg"
-as
+is
   "freeleft"
 
 lemma [quot_respect]:
@@ -231,7 +231,7 @@
 
 quotient_definition
   "right:: msg \<Rightarrow> msg"
-as
+is
   "freeright"
 
 text{*Now prove the four equations for @{term right}*}
@@ -365,7 +365,7 @@
 
 quotient_definition
   "discrim:: msg \<Rightarrow> int"
-as
+is
   "freediscrim"
 
 text{*Now prove the four equations for @{term discrim}*}