--- a/LFex.thy	Fri Dec 04 09:08:51 2009 +0100
+++ b/LFex.thy	Fri Dec 04 09:25:27 2009 +0100
@@ -181,35 +181,35 @@
   "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
 
 (* TODO/FIXME: Think whether these RSP theorems are true. *)
-lemma kpi_rsp[quot_rsp]: 
+lemma kpi_rsp[quotient_rsp]: 
   "(aty ===> op = ===> akind ===> akind) KPi KPi" sorry
-lemma tconst_rsp[quot_rsp]: 
+lemma tconst_rsp[quotient_rsp]: 
   "(op = ===> aty) TConst TConst" sorry
-lemma tapp_rsp[quot_rsp]: 
+lemma tapp_rsp[quotient_rsp]: 
   "(aty ===> atrm ===> aty) TApp TApp" sorry
-lemma tpi_rsp[quot_rsp]: 
+lemma tpi_rsp[quotient_rsp]: 
   "(aty ===> op = ===> aty ===> aty) TPi TPi" sorry
-lemma var_rsp[quot_rsp]: 
+lemma var_rsp[quotient_rsp]: 
   "(op = ===> atrm) Var Var" sorry
-lemma app_rsp[quot_rsp]: 
+lemma app_rsp[quotient_rsp]: 
   "(atrm ===> atrm ===> atrm) App App" sorry
-lemma const_rsp[quot_rsp]: 
+lemma const_rsp[quotient_rsp]: 
   "(op = ===> atrm) Const Const" sorry
-lemma lam_rsp[quot_rsp]: 
+lemma lam_rsp[quotient_rsp]: 
   "(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorry
 
-lemma perm_kind_rsp[quot_rsp]: 
+lemma perm_kind_rsp[quotient_rsp]: 
   "(op = ===> akind ===> akind) op \<bullet> op \<bullet>" sorry
-lemma perm_ty_rsp[quot_rsp]: 
+lemma perm_ty_rsp[quotient_rsp]: 
   "(op = ===> aty ===> aty) op \<bullet> op \<bullet>" sorry
-lemma perm_trm_rsp[quot_rsp]: 
+lemma perm_trm_rsp[quotient_rsp]: 
   "(op = ===> atrm ===> atrm) op \<bullet> op \<bullet>" sorry
 
-lemma fv_ty_rsp[quot_rsp]: 
+lemma fv_ty_rsp[quotient_rsp]: 
   "(aty ===> op =) fv_ty fv_ty" sorry
-lemma fv_kind_rsp[quot_rsp]: 
+lemma fv_kind_rsp[quotient_rsp]: 
   "(akind ===> op =) fv_kind fv_kind" sorry
-lemma fv_trm_rsp[quot_rsp]: 
+lemma fv_trm_rsp[quotient_rsp]: 
   "(atrm ===> op =) fv_trm fv_trm" sorry
 
 
@@ -261,7 +261,7 @@
 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
 prefer 2
-apply(tactic {* clean_tac @{context} quot 1 *})
+apply(tactic {* clean_tac @{context} 1 *})
 (*
 Profiling:
 ML_prf {* fun ith i =  (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *}
@@ -270,8 +270,8 @@
 ML_prf {* PolyML.profiling 1 *}
 ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *}
 *)
-apply(tactic {* all_inj_repabs_tac' @{context} quot rel_refl trans2 1 *})
-(*apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *})*)
+apply(tactic {* all_inj_repabs_tac' @{context} rel_refl trans2 1 *})
+(*apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})*)
 done
 
 (* Does not work:
@@ -298,7 +298,7 @@
   \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2);
   \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk>
   \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm"
-apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} @{thms alpha_EQUIVs} quot 1 *})
+apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} @{thms alpha_EQUIVs} 1 *})
 done
 
 print_quotients