diff -r 93c9022ba5e9 -r c4001cda9da3 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Fri Feb 12 15:50:43 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Fri Feb 12 16:04:10 2010 +0100
@@ -150,27 +150,27 @@
 
 quotient_definition
   "Vr1 :: name \<Rightarrow> trm1"
-as
+is
   "rVr1"
 
 quotient_definition
   "Ap1 :: trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"
-as
+is
   "rAp1"
 
 quotient_definition
   "Lm1 :: name \<Rightarrow> trm1 \<Rightarrow> trm1"
-as
+is
   "rLm1"
 
 quotient_definition
   "Lt1 :: bp \<Rightarrow> trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"
-as
+is
   "rLt1"
 
 quotient_definition
   "fv_trm1 :: trm1 \<Rightarrow> atom set"
-as
+is
   "rfv_trm1"
 
 lemma alpha_rfv1:
@@ -211,7 +211,7 @@
 
 quotient_definition
   "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1"
-as
+is
   "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"
 
 lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted]
@@ -705,42 +705,42 @@
 
 quotient_definition
   "Vr5 :: name \<Rightarrow> trm5"
-as
+is
   "rVr5"
 
 quotient_definition
   "Ap5 :: trm5 \<Rightarrow> trm5 \<Rightarrow> trm5"
-as
+is
   "rAp5"
 
 quotient_definition
   "Lt5 :: lts \<Rightarrow> trm5 \<Rightarrow> trm5"
-as
+is
   "rLt5"
 
 quotient_definition
   "Lnil :: lts"
-as
+is
   "rLnil"
 
 quotient_definition
   "Lcons :: name \<Rightarrow> trm5 \<Rightarrow> lts \<Rightarrow> lts"
-as
+is
   "rLcons"
 
 quotient_definition
    "fv_trm5 :: trm5 \<Rightarrow> atom set"
-as
+is
   "rfv_trm5"
 
 quotient_definition
    "fv_lts :: lts \<Rightarrow> atom set"
-as
+is
   "rfv_lts"
 
 quotient_definition
    "bv5 :: lts \<Rightarrow> atom set"
-as
+is
   "rbv5"
 
 lemma rbv5_eqvt:
@@ -827,12 +827,12 @@
 
 quotient_definition
   "permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5"
-as
+is
   "permute :: perm \<Rightarrow> rtrm5 \<Rightarrow> rtrm5"
 
 quotient_definition
   "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts"
-as
+is
   "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts"
 
 lemma trm5_lts_zero:
@@ -995,27 +995,27 @@
 
 quotient_definition
   "Vr6 :: name \<Rightarrow> trm6"
-as
+is
   "rVr6"
 
 quotient_definition
   "Lm6 :: name \<Rightarrow> trm6 \<Rightarrow> trm6"
-as
+is
   "rLm6"
 
 quotient_definition
   "Lt6 :: trm6 \<Rightarrow> trm6 \<Rightarrow> trm6"
-as
+is
   "rLt6"
 
 quotient_definition
    "fv_trm6 :: trm6 \<Rightarrow> atom set"
-as
+is
   "rfv_trm6"
 
 quotient_definition
    "bv6 :: trm6 \<Rightarrow> atom set"
-as
+is
   "rbv6"
 
 lemma [quot_respect]:
@@ -1077,7 +1077,7 @@
 
 quotient_definition
   "permute_trm6 :: perm \<Rightarrow> trm6 \<Rightarrow> trm6"
-as
+is
   "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"
 
 instance
@@ -1316,32 +1316,32 @@
 
 quotient_definition
   "qVar9 :: name \<Rightarrow> lam9"
-as
+is
   "Var9"
 
 quotient_definition
   "qLam :: name \<Rightarrow> lam9 \<Rightarrow> lam9"
-as
+is
   "Lam9"
 
 quotient_definition
   "qBla9 :: lam9 \<Rightarrow> lam9 \<Rightarrow> bla9"
-as
+is
   "Bla9"
 
 quotient_definition
   "fv_lam9 :: lam9 \<Rightarrow> atom set"
-as
+is
   "rfv_lam9"
 
 quotient_definition
   "fv_bla9 :: bla9 \<Rightarrow> atom set"
-as
+is
   "rfv_bla9"
 
 quotient_definition
   "bv9 :: lam9 \<Rightarrow> atom set"
-as
+is
   "rbv9"
 
 instantiation lam9 and bla9 :: pt
@@ -1349,12 +1349,12 @@
 
 quotient_definition
   "permute_lam9 :: perm \<Rightarrow> lam9 \<Rightarrow> lam9"
-as
+is
   "permute :: perm \<Rightarrow> rlam9 \<Rightarrow> rlam9"
 
 quotient_definition
   "permute_bla9 :: perm \<Rightarrow> bla9 \<Rightarrow> bla9"
-as
+is
   "permute :: perm \<Rightarrow> rbla9 \<Rightarrow> rbla9"
 
 instance