diff -r df053507edba -r 37285ec4387d Quot/Examples/LFex.thy
--- a/Quot/Examples/LFex.thy	Sun Dec 20 00:26:53 2009 +0100
+++ b/Quot/Examples/LFex.thy	Sun Dec 20 00:53:35 2009 +0100
@@ -81,48 +81,48 @@
     TRM = trm / atrm
   by (auto intro: alpha_equivps)
 
-quotient_def
+quotient_definition
    "TYP :: KIND"
 as
   "Type"
 
-quotient_def
+quotient_definition
    "KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
 as
   "KPi"
 
-quotient_def
+quotient_definition
    "TCONST :: ident \<Rightarrow> TY"
 as
   "TConst"
 
-quotient_def
+quotient_definition
    "TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY"
 as
   "TApp"
 
-quotient_def
+quotient_definition
    "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
 as
   "TPi"
 
 (* FIXME: does not work with CONST *)
-quotient_def
+quotient_definition
    "CONS :: ident \<Rightarrow> TRM"
 as
   "Const"
 
-quotient_def
+quotient_definition
    "VAR :: name \<Rightarrow> TRM"
 as
   "Var"
 
-quotient_def
+quotient_definition
    "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM"
 as
   "App"
 
-quotient_def
+quotient_definition
    "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
 as
   "Lam"
@@ -138,17 +138,17 @@
 thm LAM_def
 
 (* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *)
-quotient_def
+quotient_definition
    "FV_kind :: KIND \<Rightarrow> name set"
 as
   "fv_kind"
 
-quotient_def
+quotient_definition
    "FV_ty :: TY \<Rightarrow> name set"
 as
   "fv_ty"
 
-quotient_def
+quotient_definition
    "FV_trm :: TRM \<Rightarrow> name set"
 as
   "fv_trm"
@@ -164,17 +164,17 @@
     perm_trm  \<equiv> "perm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM"     (unchecked) 
 begin
 
-quotient_def
+quotient_definition
    "perm_kind :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND"
 as
   "(perm::'x prm \<Rightarrow> kind \<Rightarrow> kind)"
 
-quotient_def
+quotient_definition
    "perm_ty :: 'x prm \<Rightarrow> TY \<Rightarrow> TY"
 as
   "(perm::'x prm \<Rightarrow> ty \<Rightarrow> ty)"
 
-quotient_def
+quotient_definition
    "perm_trm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM"
 as
   "(perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"