--- a/src/ZF/Resid/Terms.ML Wed Jul 15 12:02:19 1998 +0200
+++ b/src/ZF/Resid/Terms.ML Wed Jul 15 14:13:18 1998 +0200
@@ -11,18 +11,15 @@
(* unmark simplifications *)
(* ------------------------------------------------------------------------- *)
-Goalw [unmark_def]
- "unmark(Var(n)) = Var(n)";
+Goalw [unmark_def] "unmark(Var(n)) = Var(n)";
by (Asm_simp_tac 1);
qed "unmark_Var";
-Goalw [unmark_def]
- "unmark(Fun(t)) = Fun(unmark(t))";
+Goalw [unmark_def] "unmark(Fun(t)) = Fun(unmark(t))";
by (Asm_simp_tac 1);
qed "unmark_Fun";
-Goalw [unmark_def]
- "unmark(App(b,n,m)) = App(0,unmark(n),unmark(m))";
+Goalw [unmark_def] "unmark(App(b,n,m)) = App(0,unmark(n),unmark(m))";
by (Asm_simp_tac 1);
qed "unmark_App";
@@ -42,13 +39,12 @@
(* ------------------------------------------------------------------------- *)
Goalw [unmark_def]
- "!!u. u:redexes ==> unmark(u):lambda";
+ "u:redexes ==> unmark(u):lambda";
by (eresolve_tac [redexes.induct] 1);
by (ALLGOALS Asm_simp_tac);
qed "unmark_type";
-Goal
- "!!u. u:lambda ==> unmark(u) = u";
+Goal "u:lambda ==> unmark(u) = u";
by (eresolve_tac [lambda.induct] 1);
by (ALLGOALS Asm_simp_tac);
qed "lambda_unmark";
@@ -58,15 +54,13 @@
(* lift and subst preserve lambda *)
(* ------------------------------------------------------------------------- *)
-Goal
- "!!u.[|v:lambda|]==> ALL k:nat. lift_rec(v,k):lambda";
+Goal "[|v:lambda|]==> ALL k:nat. lift_rec(v,k):lambda";
by (eresolve_tac [lambda.induct] 1);
by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()))));
qed "liftL_typea";
val liftL_type =liftL_typea RS bspec ;
-Goal
- "!!n.[|v:lambda|]==> ALL n:nat. ALL u:lambda. subst_rec(u,v,n):lambda";
+Goal "[|v:lambda|]==> ALL n:nat. ALL u:lambda. subst_rec(u,v,n):lambda";
by (eresolve_tac [lambda.induct] 1);
by (ALLGOALS(asm_full_simp_tac ((addsplit (simpset())) addsimps [liftL_type])));
qed "substL_typea";