--- a/Quot/QuotMain.thy Wed Feb 10 11:10:44 2010 +0100
+++ b/Quot/QuotMain.thy Wed Feb 10 11:11:06 2010 +0100
@@ -140,7 +140,7 @@
shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"
and QT_ex: "Quot_True (Ex P) \<Longrightarrow> Quot_True P"
and QT_ex1: "Quot_True (Ex1 P) \<Longrightarrow> Quot_True P"
- and QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True (P x))"
+ and QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True (P x))"
and QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)"
by (simp_all add: Quot_True_def ext)
@@ -169,7 +169,7 @@
{* Sets up the three goals for the lifting procedure. *}
method_setup regularize =
- {* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac) *}
+ {* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac) *}
{* Proves automatically the regularization goals from the lifting procedure. *}
method_setup injection =
--- a/Quot/quotient_tacs.ML Wed Feb 10 11:10:44 2010 +0100
+++ b/Quot/quotient_tacs.ML Wed Feb 10 11:11:06 2010 +0100
@@ -29,7 +29,7 @@
(* Since HOL_basic_ss is too "big" for us, we *)
(* need to set up our own minimal simpset. *)
-fun mk_minimal_ss ctxt =
+fun mk_minimal_ss ctxt =
Simplifier.context ctxt empty_ss
setsubgoaler asm_simp_tac
setmksimps (mksimps [])
--- a/Quot/quotient_term.ML Wed Feb 10 11:10:44 2010 +0100
+++ b/Quot/quotient_term.ML Wed Feb 10 11:11:06 2010 +0100
@@ -90,7 +90,7 @@
TVar _ => mk_Free rty
| Type (_, []) => mk_identity rty
| Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
- | _ => raise LIFT_MATCH ("mk_mapfun (default)")
+ | _ => raise LIFT_MATCH "mk_mapfun (default)"
in
fold_rev Term.lambda vs' (mk_mapfun_aux rty)
end
@@ -706,7 +706,7 @@
| x => x)
(* subst_trms takes a list of (rtrm, qtrm) substitution pairs
- and if the given term matches any of the raw terms it
+ and if the given term matches any of the raw terms it
returns the appropriate qtrm instantiated. If none of
them matched it returns NONE. *)
fun subst_trm thy t (rtrm, qtrm) s =