--- a/src/HOLCF/Lift3.ML Thu Apr 24 18:06:46 1997 +0200
+++ b/src/HOLCF/Lift3.ML Thu Apr 24 18:07:35 1997 +0200
@@ -25,22 +25,22 @@
local
val case1' = prove_goal thy "lift_case f1 f2 UU = f1"
- (fn _ => [simp_tac (!simpset addsimps lift.simps) 1]);
+ (fn _ => [simp_tac (!simpset addsimps lift.simps) 1]);
val case2' = prove_goal thy "lift_case f1 f2 (Def a) = f2 a"
- (fn _ => [Simp_tac 1]);
+ (fn _ => [Simp_tac 1]);
val distinct1' = prove_goal thy "UU ~= Def a"
- (fn _ => [Simp_tac 1]);
+ (fn _ => [Simp_tac 1]);
val distinct2' = prove_goal thy "Def a ~= UU"
- (fn _ => [Simp_tac 1]);
+ (fn _ => [Simp_tac 1]);
val inject' = prove_goal thy "Def a = Def aa = (a = aa)"
- (fn _ => [Simp_tac 1]);
+ (fn _ => [Simp_tac 1]);
val rec1' = prove_goal thy "lift_rec f1 f2 UU = f1"
- (fn _ => [Simp_tac 1]);
+ (fn _ => [Simp_tac 1]);
val rec2' = prove_goal thy "lift_rec f1 f2 (Def a) = f2 a"
- (fn _ => [Simp_tac 1]);
+ (fn _ => [Simp_tac 1]);
val induct' = prove_goal thy "[| P UU; !a. P (Def a) |] ==> P lift"
- (fn prems => [cut_facts_tac prems 1, Asm_full_simp_tac 1,
- etac Lift1.lift.induct 1,fast_tac HOL_cs 1]);
+ (fn prems => [cut_facts_tac prems 1, Asm_full_simp_tac 1,
+ etac Lift1.lift.induct 1,fast_tac HOL_cs 1]);
in
@@ -228,14 +228,14 @@
cont_fapp_app,cont_fapp_app_app,cont_if];
val cont_lemmas2 = cont_lemmas1 @ cont_lemmas_ext;
-
-Addsimps cont_lemmas_ext;
+
+Addsimps cont_lemmas_ext;
fun cont_tac i = resolve_tac cont_lemmas2 i;
fun cont_tacR i = REPEAT (cont_tac i);
fun cont_tacRs i = simp_tac (!simpset addsimps [flift1_def,flift2_def]) i THEN
- REPEAT (cont_tac i);
+ REPEAT (cont_tac i);
simpset := !simpset addSolver (K (DEPTH_SOLVE_1 o cont_tac));