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