src/ZF/Resid/Reduction.ML

--- a/src/ZF/Resid/Reduction.ML	Mon Sep 29 11:51:09 1997 +0200
+++ b/src/ZF/Resid/Reduction.ML	Mon Sep 29 11:51:52 1997 +0200
@@ -41,34 +41,34 @@
 by (etac Sred.induct 1);
 by (resolve_tac [Sred.trans] 3);
 by (ALLGOALS (Asm_simp_tac ));
-val red_Fun = result();
+qed "red_Fun";
 
 goal Reduction.thy  
     "!!u.[|n:lambda; m ---> m'|]==> Apl(m,n)--->Apl(m',n)";
 by (etac Sred.induct 1);
 by (resolve_tac [Sred.trans] 3);
 by (ALLGOALS (Asm_simp_tac ));
-val red_Apll = result();
+qed "red_Apll";
 
 goal Reduction.thy  
     "!!u.[|n:lambda; m ---> m'|]==> Apl(n,m)--->Apl(n,m')";
 by (etac Sred.induct 1);
 by (resolve_tac [Sred.trans] 3);
 by (ALLGOALS (Asm_simp_tac ));
-val red_Aplr = result();
+qed "red_Aplr";
 
 goal Reduction.thy  
     "!!u.[|m ---> m'; n--->n'|]==> Apl(m,n)--->Apl(m',n')";
 by (res_inst_tac [("n","Apl(m',n)")] Sred.trans 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [red_Apll,red_Aplr]) ));
-val red_Apl = result();
+qed "red_Apl";
 
 goal Reduction.thy  
     "!!u.[|m:lambda; m':lambda; n:lambda; n':lambda; m ---> m'; n--->n'|]==> \
 \              Apl(Fun(m),n)---> n'/m'";
 by (res_inst_tac [("n","Apl(Fun(m'),n')")] Sred.trans 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [red_Apl,red_Fun]) ));
-val red_beta = result();
+qed "red_beta";
 
 
 (* ------------------------------------------------------------------------- *)
@@ -79,25 +79,25 @@
 goal Reduction.thy "!!u.m:lambda==> m =1=> m";
 by (eresolve_tac [lambda.induct] 1);
 by (ALLGOALS (Asm_simp_tac ));
-val refl_par_red1 = result();
+qed "refl_par_red1";
 
 goal Reduction.thy "!!u.m-1->n ==> m=1=>n";
 by (etac Sred1.induct 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [refl_par_red1]) ));
-val red1_par_red1 = result();
+qed "red1_par_red1";
 
 goal Reduction.thy "!!u.m--->n ==> m===>n";
 by (etac Sred.induct 1);
 by (resolve_tac [Spar_red.trans] 3);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [refl_par_red1,red1_par_red1]) ));
-val red_par_red = result();
+qed "red_par_red";
 
 goal Reduction.thy "!!u.m===>n ==> m--->n";
 by (etac Spar_red.induct 1);
 by (etac Spar_red1.induct 1);
 by (resolve_tac [Sred.trans] 5);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [red_Fun,red_beta,red_Apl]) ));
-val par_red_red = result();
+qed "par_red_red";
 
 
 (* ------------------------------------------------------------------------- *)
@@ -107,11 +107,11 @@
 goal Reduction.thy  
     "!!u.m=1=>n ==> EX v. m|>v = n & m~v & regular(v)";
 by (etac Spar_red1.induct 1);
-by (step_tac (!claset) 1);
+by Safe_tac;
 by (ALLGOALS (REPEAT o (resolve_tac [exI,conjI])));
 by (TRYALL(resolve_tac [res_redex,res_App,res_Fun,res_Var]));
 by (ALLGOALS (asm_simp_tac (!simpset)));
-val simulation = result();
+qed "simulation";
 
 
 (* ------------------------------------------------------------------------- *)
@@ -123,7 +123,7 @@
 \           ALL k:nat. unmark(lift_rec(u,k)) = lift_rec(unmark(u),k)";
 by (eresolve_tac [redexes.induct] 1);
 by (ALLGOALS (asm_full_simp_tac (addsplit (!simpset))));
-val unmmark_lift_rec = result();
+qed "unmmark_lift_rec";
 
 goal Reduction.thy  
     "!!u.v:redexes ==> ALL k:nat.ALL u:redexes.  \
@@ -131,7 +131,7 @@
 by (eresolve_tac [redexes.induct] 1);
 by (ALLGOALS (asm_full_simp_tac 
              ((addsplit (!simpset)) addsimps [unmmark_lift_rec])));
-val unmmark_subst_rec = result();
+qed "unmmark_subst_rec";
 
 
 (* ------------------------------------------------------------------------- *)
@@ -144,10 +144,11 @@
 by (ALLGOALS (asm_full_simp_tac (reducL_ss addsimps [unmmark_subst_rec]) ));
 by (dres_inst_tac [("psi", "Fun(?u) =1=> ?w")] asm_rl 1);
 by (asm_full_simp_tac reducL_ss 1);
-val completeness_l = result();
+qed_spec_mp "completeness_l";
 
 goal Reduction.thy  
     "!!u.[|u:lambda; u~v; regular(v)|]==> u =1=> unmark(u|>v)";
-by (dres_inst_tac [("u1","u")] (completeness_l RS mp) 1);
+by (dtac completeness_l 1);
 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [lambda_unmark]) ));
-val completeness = result();
+qed "completeness";
+