--- a/Quot/Examples/FSet.thy	Fri Feb 12 15:50:43 2010 +0100
+++ b/Quot/Examples/FSet.thy	Fri Feb 12 16:04:10 2010 +0100
@@ -28,17 +28,17 @@
 
 quotient_definition
    "EMPTY :: 'a fset"
-as
+is
   "[]::'a list"
 
 quotient_definition
    "INSERT :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-as
+is
   "op #"
 
 quotient_definition
    "FUNION :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-as
+is
   "op @"
 
 fun
@@ -49,12 +49,12 @@
 
 quotient_definition
    "CARD :: 'a fset \<Rightarrow> nat"
-as
+is
   "card1"
 
 quotient_definition
   "fconcat :: ('a fset) fset \<Rightarrow> 'a fset"
-as
+is
   "concat"
 
 term concat
@@ -120,17 +120,17 @@
 
 quotient_definition
    "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
-as
+is
   "op mem"
 
 quotient_definition
    "FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a"
-as
+is
   "fold1"
 
 quotient_definition
   "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
-as
+is
   "map"
 
 lemma mem_rsp:
@@ -285,12 +285,12 @@
 
 quotient_definition
    "EMPTY2 :: 'a fset2"
-as
+is
   "[]::'a list"
 
 quotient_definition
    "INSERT2 :: 'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
-as
+is
   "op #"
 
 lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
@@ -303,12 +303,12 @@
 
 quotient_definition
   "fset_rec :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
-as
+is
   "list_rec"
 
 quotient_definition
   "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
-as
+is
   "list_case"
 
 (* Probably not true without additional assumptions about the function *)

--- a/Quot/Examples/FSet2.thy	Fri Feb 12 15:50:43 2010 +0100
+++ b/Quot/Examples/FSet2.thy	Fri Feb 12 16:04:10 2010 +0100
@@ -27,12 +27,12 @@
 
 quotient_definition
   "fempty :: 'a fset" ("{||}")
-as
+is
   "[]"
 
 quotient_definition
   "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-as
+is
   "(op #)"
 
 lemma finsert_rsp[quot_respect]:
@@ -41,7 +41,7 @@
 
 quotient_definition
   "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [65,66] 65)
-as
+is
   "(op @)"
 
 lemma append_rsp_aux1:
@@ -68,7 +68,7 @@
 
 quotient_definition
   "fmem :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50)
-as
+is
   "(op mem)"
 
 lemma memb_rsp_aux:
@@ -92,7 +92,7 @@
 
 quotient_definition
   "finter::'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)
-as
+is
   "inter_list"
 
 no_syntax

--- a/Quot/Examples/FSet3.thy	Fri Feb 12 15:50:43 2010 +0100
+++ b/Quot/Examples/FSet3.thy	Fri Feb 12 16:04:10 2010 +0100
@@ -136,7 +136,7 @@
 
 quotient_definition
   "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "|\<union>|" 65)
-as
+is
   "op @"
 
 section {* Cardinality of finite sets *}
@@ -227,12 +227,12 @@
 
 quotient_definition
   "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
-as
+is
  "map"
 
 quotient_definition
   "fconcat :: ('a fset) fset => 'a fset"
-as
+is
  "concat"
 
 (*lemma fconcat_rsp[quot_respect]:
@@ -619,19 +619,19 @@
 
 quotient_definition
   "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" 
-  as "delete_raw"
+  is "delete_raw"
 
 quotient_definition
   "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)
-  as "inter_raw"
+  is "inter_raw"
 
 quotient_definition
   "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" 
-  as "fold_raw"
+  is "fold_raw"
 
 quotient_definition
   "fset_to_set :: 'a fset \<Rightarrow> 'a set" 
-  as "set"
+  is "set"
 
 
 section {* Lifted Theorems *}
@@ -690,7 +690,7 @@
 
 quotient_definition
   "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
-as
+is
   "list_case"
 
 (* NOT SURE IF TRUE *)

--- a/Quot/Examples/IntEx.thy	Fri Feb 12 15:50:43 2010 +0100
+++ b/Quot/Examples/IntEx.thy	Fri Feb 12 16:04:10 2010 +0100
@@ -15,12 +15,12 @@
 
 quotient_definition
   "ZERO :: my_int"
-as
+is
   "(0::nat, 0::nat)"
 
 quotient_definition
   "ONE :: my_int"
-as
+is
   "(1::nat, 0::nat)"
 
 fun
@@ -30,7 +30,7 @@
 
 quotient_definition
   "PLUS :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
-as
+is
   "my_plus"
 
 fun
@@ -40,7 +40,7 @@
 
 quotient_definition
   "NEG :: my_int \<Rightarrow> my_int"
-as
+is
   "my_neg"
 
 definition
@@ -55,7 +55,7 @@
 
 quotient_definition
   "MULT :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
-as
+is
   "my_mult"
 
 
@@ -67,7 +67,7 @@
 
 quotient_definition
    "LE :: my_int \<Rightarrow> my_int \<Rightarrow> bool"
-as
+is
   "my_le"
 
 term LE

--- a/Quot/Examples/IntEx2.thy	Fri Feb 12 15:50:43 2010 +0100
+++ b/Quot/Examples/IntEx2.thy	Fri Feb 12 16:04:10 2010 +0100
@@ -21,10 +21,10 @@
 ML {* @{term "0 \<Colon> int"} *}
 
 quotient_definition
-  "0 \<Colon> int" as "(0\<Colon>nat, 0\<Colon>nat)"
+  "0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)"
 
 quotient_definition
-  "1 \<Colon> int" as "(1\<Colon>nat, 0\<Colon>nat)"
+  "1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)"
 
 fun
   plus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
@@ -32,7 +32,7 @@
   "plus_raw (x, y) (u, v) = (x + u, y + v)"
 
 quotient_definition
-  "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" as "plus_raw"
+  "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" is "plus_raw"
 
 fun
   uminus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
@@ -40,7 +40,7 @@
   "uminus_raw (x, y) = (y, x)"
 
 quotient_definition
-  "(uminus \<Colon> (int \<Rightarrow> int))" as "uminus_raw"
+  "(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_raw"
 
 definition
   minus_int_def [code del]:  "z - w = z + (-w\<Colon>int)"
@@ -51,7 +51,7 @@
   "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
 quotient_definition
-  mult_int_def: "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" as "mult_raw"
+  mult_int_def: "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" is "mult_raw"
 
 fun
   le_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
@@ -59,7 +59,7 @@
   "le_raw (x, y) (u, v) = (x+v \<le> u+y)"
 
 quotient_definition
-  le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" as "le_raw"
+  le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_raw"
 
 definition
   less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
@@ -207,7 +207,7 @@
   "int_of_nat_raw m = (m :: nat, 0 :: nat)"
 
 quotient_definition
-  "int_of_nat :: nat \<Rightarrow> int" as "int_of_nat_raw"
+  "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw"
 
 lemma[quot_respect]: 
   shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"

--- a/Quot/Examples/LFex.thy	Fri Feb 12 15:50:43 2010 +0100
+++ b/Quot/Examples/LFex.thy	Fri Feb 12 16:04:10 2010 +0100
@@ -83,48 +83,48 @@
 
 quotient_definition
    "TYP :: KIND"
-as
+is
   "Type"
 
 quotient_definition
    "KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
-as
+is
   "KPi"
 
 quotient_definition
    "TCONST :: ident \<Rightarrow> TY"
-as
+is
   "TConst"
 
 quotient_definition
    "TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY"
-as
+is
   "TApp"
 
 quotient_definition
    "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
-as
+is
   "TPi"
 
 (* FIXME: does not work with CONST *)
 quotient_definition
    "CONS :: ident \<Rightarrow> TRM"
-as
+is
   "Const"
 
 quotient_definition
    "VAR :: name \<Rightarrow> TRM"
-as
+is
   "Var"
 
 quotient_definition
    "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"
-as
+is
   "App"
 
 quotient_definition
    "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
-as
+is
   "Lam"
 
 thm TYP_def
@@ -140,17 +140,17 @@
 (* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *)
 quotient_definition
    "FV_kind :: KIND \<Rightarrow> name set"
-as
+is
   "fv_kind"
 
 quotient_definition
    "FV_ty :: TY \<Rightarrow> name set"
-as
+is
   "fv_ty"
 
 quotient_definition
    "FV_trm :: TRM \<Rightarrow> name set"
-as
+is
   "fv_trm"
 
 thm FV_kind_def
@@ -166,17 +166,17 @@
 
 quotient_definition
    "perm_kind :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND"
-as
+is
   "(perm::'x prm \<Rightarrow> kind \<Rightarrow> kind)"
 
 quotient_definition
    "perm_ty :: 'x prm \<Rightarrow> TY \<Rightarrow> TY"
-as
+is
   "(perm::'x prm \<Rightarrow> ty \<Rightarrow> ty)"
 
 quotient_definition
    "perm_trm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM"
-as
+is
   "(perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
 
 end

--- a/Quot/Examples/LamEx.thy	Fri Feb 12 15:50:43 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Fri Feb 12 16:04:10 2010 +0100
@@ -178,22 +178,22 @@
 
 quotient_definition
   "Var :: name \<Rightarrow> lam"
-as
+is
   "rVar"
 
 quotient_definition
    "App :: lam \<Rightarrow> lam \<Rightarrow> lam"
-as
+is
   "rApp"
 
 quotient_definition
   "Lam :: name \<Rightarrow> lam \<Rightarrow> lam"
-as
+is
   "rLam"
 
 quotient_definition
   "fv :: lam \<Rightarrow> name set"
-as
+is
   "rfv"
 
 (* definition of overloaded permutation function *)
@@ -204,7 +204,7 @@
 
 quotient_definition
   "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"
-as
+is
   "perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam"
 
 end

--- 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}*}

--- a/Quot/Examples/LarryInt.thy	Fri Feb 12 15:50:43 2010 +0100
+++ b/Quot/Examples/LarryInt.thy	Fri Feb 12 16:04:10 2010 +0100
@@ -16,18 +16,18 @@
 instantiation int :: "{zero, one, plus, uminus, minus, times, ord}"
 begin
 
-quotient_definition 
-  Zero_int_def: "0::int" as "(0::nat, 0::nat)"
+quotient_definition
+  Zero_int_def: "0::int" is "(0::nat, 0::nat)"
 
 quotient_definition
-  One_int_def: "1::int" as "(1::nat, 0::nat)"
+  One_int_def: "1::int" is "(1::nat, 0::nat)"
 
 definition
   "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))"
 
 quotient_definition
   "(op +) :: int \<Rightarrow> int \<Rightarrow> int" 
-as 
+is
   "add_raw"
 
 definition
@@ -35,7 +35,7 @@
 
 quotient_definition
   "uminus :: int \<Rightarrow> int" 
-as 
+is
   "uminus_raw"
 
 fun
@@ -45,7 +45,7 @@
 
 quotient_definition
   "(op *) :: int \<Rightarrow> int \<Rightarrow> int" 
-as 
+is
   "mult_raw"
 
 definition
@@ -53,7 +53,7 @@
 
 quotient_definition 
   le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" 
-as 
+is
   "le_raw"
 
 definition
@@ -369,7 +369,7 @@
 
 quotient_definition
   "nat2::int \<Rightarrow> nat"
-as
+is
   "nat_raw"
 
 abbreviation

--- a/Quot/Examples/SigmaEx.thy	Fri Feb 12 15:50:43 2010 +0100
+++ b/Quot/Examples/SigmaEx.thy	Fri Feb 12 16:04:10 2010 +0100
@@ -35,27 +35,27 @@
 
 quotient_definition
   "Var :: name \<Rightarrow> obj"
-as
+is
   "rVar"
 
 quotient_definition
   "Obj :: (string \<times> method) list \<Rightarrow> obj"
-as
+is
   "rObj"
 
 quotient_definition
   "Inv :: obj \<Rightarrow> string \<Rightarrow> obj"
-as
+is
   "rInv"
 
 quotient_definition
   "Upd :: obj \<Rightarrow> string \<Rightarrow> method \<Rightarrow> obj"
-as
+is
   "rUpd"
 
 quotient_definition
   "Sig :: name \<Rightarrow> obj \<Rightarrow> method"
-as
+is
   "rSig"
 
 overloading
@@ -65,12 +65,12 @@
 
 quotient_definition
   "perm_obj :: 'x prm \<Rightarrow> obj \<Rightarrow> obj"
-as
+is
   "(perm::'x prm \<Rightarrow> robj \<Rightarrow> robj)"
 
 quotient_definition
   "perm_method :: 'x prm \<Rightarrow> method \<Rightarrow> method"
-as
+is
   "(perm::'x prm \<Rightarrow> rmethod \<Rightarrow> rmethod)"
 
 end

--- a/Quot/Nominal/Abs.thy	Fri Feb 12 15:50:43 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Fri Feb 12 16:04:10 2010 +0100
@@ -194,9 +194,9 @@
   done
 
 quotient_definition
-   "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs"
-as
-   "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
+  "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs"
+is
+  "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
 
 lemma [quot_respect]:
   shows "((op =) ===> (op =) ===> alpha_abs) Pair Pair"
@@ -234,7 +234,7 @@
 
 quotient_definition
   "permute_abs::perm \<Rightarrow> ('a::pt abs) \<Rightarrow> 'a abs"
-as
+is
   "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
 
 lemma permute_ABS [simp]:
@@ -252,7 +252,7 @@
 
 quotient_definition
   "supp_Abs_fun :: ('a::pt) abs \<Rightarrow> atom \<Rightarrow> bool"
-as
+is
   "supp_abs_fun"
 
 lemma supp_Abs_fun_simp:

--- a/Quot/Nominal/LFex.thy	Fri Feb 12 15:50:43 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Fri Feb 12 16:04:10 2010 +0100
@@ -256,64 +256,64 @@
 
 quotient_definition
    "TYP :: KIND"
-as
+is
   "Type"
 
 quotient_definition
    "KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
-as
+is
   "KPi"
 
 quotient_definition
    "TCONST :: ident \<Rightarrow> TY"
-as
+is
   "TConst"
 
 quotient_definition
    "TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY"
-as
+is
   "TApp"
 
 quotient_definition
    "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
-as
+is
   "TPi"
 
 (* FIXME: does not work with CONST *)
 quotient_definition
    "CONS :: ident \<Rightarrow> TRM"
-as
+is
   "Const"
 
 quotient_definition
    "VAR :: name \<Rightarrow> TRM"
-as
+is
   "Var"
 
 quotient_definition
    "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"
-as
+is
   "App"
 
 quotient_definition
    "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
-as
+is
   "Lam"
 
 (* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *)
 quotient_definition
    "fv_kind :: KIND \<Rightarrow> atom set"
-as
+is
   "rfv_kind"
 
 quotient_definition
    "fv_ty :: TY \<Rightarrow> atom set"
-as
+is
   "rfv_ty"
 
 quotient_definition
    "fv_trm :: TRM \<Rightarrow> atom set"
-as
+is
   "rfv_trm"
 
 lemma alpha_rfv:
@@ -390,17 +390,17 @@
 
 quotient_definition
   "permute_KIND :: perm \<Rightarrow> KIND \<Rightarrow> KIND"
-as
+is
   "permute :: perm \<Rightarrow> kind \<Rightarrow> kind"
 
 quotient_definition
   "permute_TY :: perm \<Rightarrow> TY \<Rightarrow> TY"
-as
+is
   "permute :: perm \<Rightarrow> ty \<Rightarrow> ty"
 
 quotient_definition
   "permute_TRM :: perm \<Rightarrow> TRM \<Rightarrow> TRM"
-as
+is
   "permute :: perm \<Rightarrow> trm \<Rightarrow> trm"
 
 lemmas permute_ktt[simp] = permute_kind_permute_ty_permute_trm.simps[quot_lifted]

--- a/Quot/Nominal/LamEx.thy	Fri Feb 12 15:50:43 2010 +0100
+++ b/Quot/Nominal/LamEx.thy	Fri Feb 12 16:04:10 2010 +0100
@@ -282,22 +282,22 @@
 
 quotient_definition
   "Var :: name \<Rightarrow> lam"
-as
+is
   "rVar"
 
 quotient_definition
    "App :: lam \<Rightarrow> lam \<Rightarrow> lam"
-as
+is
   "rApp"
 
 quotient_definition
   "Lam :: name \<Rightarrow> lam \<Rightarrow> lam"
-as
+is
   "rLam"
 
 quotient_definition
   "fv :: lam \<Rightarrow> atom set"
-as
+is
   "rfv"
 
 lemma perm_rsp[quot_respect]:
@@ -346,7 +346,7 @@
 
 quotient_definition
   "permute_lam :: perm \<Rightarrow> lam \<Rightarrow> lam"
-as
+is
   "permute :: perm \<Rightarrow> rlam \<Rightarrow> rlam"
 
 lemma permute_lam [simp]:

--- a/Quot/Nominal/LamEx2.thy	Fri Feb 12 15:50:43 2010 +0100
+++ b/Quot/Nominal/LamEx2.thy	Fri Feb 12 16:04:10 2010 +0100
@@ -175,22 +175,22 @@
 
 quotient_definition
   "Var :: name \<Rightarrow> lam"
-as
+is
   "rVar"
 
 quotient_definition
    "App :: lam \<Rightarrow> lam \<Rightarrow> lam"
-as
+is
   "rApp"
 
 quotient_definition
   "Lam :: name \<Rightarrow> lam \<Rightarrow> lam"
-as
+is
   "rLam"
 
 quotient_definition
   "fv :: lam \<Rightarrow> atom set"
-as
+is
   "rfv"
 
 lemma perm_rsp[quot_respect]:
@@ -239,7 +239,7 @@
 
 quotient_definition
   "permute_lam :: perm \<Rightarrow> lam \<Rightarrow> lam"
-as
+is
   "permute :: perm \<Rightarrow> rlam \<Rightarrow> rlam"
 
 lemma permute_lam [simp]:

--- 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