diff -r 93c9022ba5e9 -r c4001cda9da3 Quot/Nominal/LFex.thy
--- 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]