Much tidying including "qed" instead of result(), and even qed_spec_mp,
and Safe_tac instead of step_tac

--- a/src/ZF/Resid/Confluence.ML	Mon Sep 29 11:51:09 1997 +0200
+++ b/src/ZF/Resid/Confluence.ML	Mon Sep 29 11:51:52 1997 +0200
@@ -8,19 +8,6 @@
 open Confluence;
 
 (* ------------------------------------------------------------------------- *)
-(*        Confluence                                                         *)
-(* ------------------------------------------------------------------------- *)
-
-goalw Confluence.thy [confluence_def] 
-    "!!u.[|confluence(Spar_red)|]==> confluence(Sred)";
-by (step_tac (!claset) 1);
-by (dres_inst_tac [("x4","x"),("x3","y"),("x1","z")] 
-    (spec RS spec RS mp RS spec RS mp) 1);
-by (ALLGOALS(asm_simp_tac (!simpset addsimps [red_par_red])));
-by (fast_tac (!claset addIs [par_red_red])  1);
-val lemma1 = result();
-
-(* ------------------------------------------------------------------------- *)
 (*        strip lemmas                                                       *)
 (* ------------------------------------------------------------------------- *)
 
@@ -30,7 +17,7 @@
 by (etac Spar_red.induct 1);
 by (Fast_tac  1);
 by (fast_tac (!claset addIs [Spar_red.trans]) 1);
-val strip_lemma_r = result();
+qed "strip_lemma_r";
 
 
 goalw Confluence.thy [confluence_def,strip_def] 
@@ -38,42 +25,37 @@
 by (resolve_tac [impI RS allI RS allI] 1);
 by (etac Spar_red.induct 1);
 by (Fast_tac  1);
-by (step_tac (!claset) 1);
+by (Clarify_tac 1);
 by (dres_inst_tac [("x1","z")] (spec RS mp) 1);
 by (REPEAT(eresolve_tac [exE,conjE] 2));
 by (dres_inst_tac [("x1","ua")] (spec RS mp) 2);
 by (fast_tac (!claset addIs [Spar_red.trans]) 3);
 by (TRYALL assume_tac );
-val strip_lemma_l = result();
+qed "strip_lemma_l";
 
 (* ------------------------------------------------------------------------- *)
 (*      Confluence                                                           *)
 (* ------------------------------------------------------------------------- *)
 
 
-goal Confluence.thy  
-    "!!u.confluence(Spar_red1)==> confluence(Spar_red)";
-by (resolve_tac [strip_lemma_r RS strip_lemma_l] 1);
-by (assume_tac 1);
-val lemma2 = result();
-
-
 goalw Confluence.thy [confluence_def] "confluence(Spar_red1)";
-by (step_tac (!claset) 1);
+by (Clarify_tac 1);
 by (forward_tac [simulation] 1);
 by (forw_inst_tac [("n","z")] simulation 1);
-by (step_tac (!claset) 1);
+by (Clarify_tac 1);
 by (forw_inst_tac [("v","va")] paving 1);
 by (TRYALL assume_tac);
-by (REPEAT(step_tac (!claset) 1));
-by (res_inst_tac [("v","vu")] completeness 1);
-by (ALLGOALS(asm_simp_tac (!simpset addsimps [completeness])));
-val parallel_moves = result();
+by (fast_tac (!claset addIs [completeness] addss (!simpset)) 1);
+qed "parallel_moves";
+
+bind_thm ("confluence_parallel_reduction",
+	  parallel_moves RS strip_lemma_r RS strip_lemma_l);
 
-goal Confluence.thy  "confluence(Spar_red)";
-by (resolve_tac [parallel_moves RS lemma2] 1);
-val confluence_parallel_reduction = result();
+goalw Confluence.thy [confluence_def] 
+    "!!u.[|confluence(Spar_red)|]==> confluence(Sred)";
+by(blast_tac (!claset addIs [par_red_red, red_par_red]) 1);
+val lemma1 = result();
 
-goal Confluence.thy  "confluence(Sred)";
-by (resolve_tac [confluence_parallel_reduction RS lemma1] 1);
-val confluence_beta_reduction = result();
+bind_thm ("confluence_beta_reduction",
+	  confluence_parallel_reduction RS lemma1);
+

--- a/src/ZF/Resid/Conversion.ML	Mon Sep 29 11:51:09 1997 +0200
+++ b/src/ZF/Resid/Conversion.ML	Mon Sep 29 11:51:52 1997 +0200
@@ -7,15 +7,14 @@
 
 open Conversion;
 
-val (!simpset) = (!simpset) addsimps (Sconv1.intrs@[Sconv.one_step,Sconv.refl]);
+AddIs (Sconv.intrs @ Sconv1.intrs);
 
 goal Conversion.thy  
     "!!u.m<--->n ==> n<--->m";
 by (etac Sconv.induct 1);
 by (etac Sconv1.induct 1);
-by (resolve_tac [Sconv.trans] 4);
-by (ALLGOALS(asm_simp_tac (!simpset) ));
-val conv_sym = result();
+by (ALLGOALS Blast_tac);
+qed "conv_sym";
 
 (* ------------------------------------------------------------------------- *)
 (*      Church_Rosser Theorem                                                *)
@@ -25,20 +24,11 @@
     "!!u.m<--->n ==> EX p.(m --->p) & (n ---> p)";
 by (etac Sconv.induct 1);
 by (etac Sconv1.induct 1);
-by (fast_tac (!claset addIs [red1D1,redD2]) 1);
-by (fast_tac (!claset addIs [red1D1,redD2]) 1);
-by (fast_tac (!claset addIs [red1D1,redD2]) 1);
+by (blast_tac (!claset addIs [red1D1,redD2]) 1);
+by (blast_tac (!claset addIs [red1D1,redD2]) 1);
+by (blast_tac (!claset addIs [red1D1,redD2]) 1);
 by (cut_facts_tac [confluence_beta_reduction]  1);
 by (rewtac confluence_def);
-by (step_tac (!claset) 1);
-by (dres_inst_tac [("x4","n"),("x3","pa"),("x1","pb")] 
-    (spec RS spec RS mp RS spec RS mp) 1);
-by (TRYALL assume_tac);
-by (step_tac (!claset) 1);
-by (step_tac (!claset) 1);
-by (step_tac (!claset) 1);
-by (res_inst_tac [("n","pa")]Sred.trans 1);
-by (res_inst_tac [("n","pb"),("p","ua")] Sred.trans 3);
-by (TRYALL assume_tac);
-val Church_Rosser = result();
+by (blast_tac (!claset addIs [Sred.trans]) 1);
+qed "Church_Rosser";
 

--- a/src/ZF/Resid/Cube.ML	Mon Sep 29 11:51:09 1997 +0200
+++ b/src/ZF/Resid/Cube.ML	Mon Sep 29 11:51:52 1997 +0200
@@ -16,32 +16,29 @@
 (*         =============                                                     *)
 (* ------------------------------------------------------------------------- *)
 
-(* Having more ssumptions than needed -- removed below  *)
+(* Having more assumptions than needed -- removed below  *)
 goal Cube.thy 
     "!!u.v<==u ==> \
 \   regular(u)-->(ALL w.w~v-->w~u-->  \
 \             w |> u = (w|>v) |> (u|>v))";
 by (etac Ssub.induct 1);
-by (asm_simp_tac prism_ss 1);
-by (asm_simp_tac prism_ss 1);
-by (asm_simp_tac prism_ss 1);
+by (ALLGOALS (asm_simp_tac prism_ss));
 by (dresolve_tac [spec RS mp RS mp] 1 THEN resolve_tac [Scomp.Comp_Fun] 1 
     THEN resolve_tac [Scomp.Comp_Fun] 2 THEN (REPEAT(assume_tac 1)));
 by (asm_full_simp_tac prism_ss 1);
-by (asm_simp_tac prism_ss 1);
 by (dresolve_tac [spec RS mp RS mp] 1 THEN resolve_tac [Scomp.Comp_Fun] 1 
     THEN resolve_tac [Scomp.Comp_Fun] 2 THEN (REPEAT(assume_tac 1)));
 by (asm_full_simp_tac prism_ss 1);
-val prism_l = result();
+qed_spec_mp "prism_l";
 
 goal Cube.thy 
     "!!u.[|v <== u; regular(u); w~v|]==> \
 \       w |> u = (w|>v) |> (u|>v)";
-by (resolve_tac [prism_l RS mp RS spec RS mp RS mp ] 1);
+by (resolve_tac [prism_l] 1);
 by (rtac comp_trans 4);
 by (assume_tac 4);
 by (ALLGOALS(asm_simp_tac prism_ss));
-val prism = result();
+qed "prism";
 
 
 (* ------------------------------------------------------------------------- *)
@@ -51,11 +48,10 @@
 goal Cube.thy 
     "!!u.[|u~v; regular(v); regular(u); w~u|]==>  \
 \          (w|>u) |> (v|>u) = (w|>v) |> (u|>v)";
-by (res_inst_tac [("u2","u"),("v2","v")](preservation RS ssubst) 1 
+by (rtac (preservation RS ssubst) 1 
     THEN assume_tac 1 THEN assume_tac 1);
-by (res_inst_tac [("u2","v"),("v2","u")](preservation RS ssubst) 1);
-by (etac comp_sym 1);
-by (atac 1);
+by (rtac (preservation RS ssubst) 1 
+    THEN etac comp_sym 1 THEN assume_tac 1);
 by (stac (prism RS sym) 1);
 by (asm_full_simp_tac (!simpset addsimps 
 		       [prism RS sym,union_l,union_preserve_regular,
@@ -65,7 +61,7 @@
 		       [union_preserve_regular, comp_sym_iff]) 1);
 by (etac comp_trans 1);
 by (atac 1);
-val cube = result();
+qed "cube";
 
 
 (* ------------------------------------------------------------------------- *)
@@ -76,19 +72,11 @@
     "!!u.[|w~u; w~v; regular(u); regular(v)|]==> \
 \          EX uv vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu &\
 \            regular(vu) & (w|>v)~uv & regular(uv) ";
-by (forw_inst_tac [("x1","v")] (comp_sym RS comp_trans) 1);
-by (step_tac (!claset addSIs [exI]) 1);
+by (subgoal_tac "u~v" 1);
+by (safe_tac (!claset addSIs [exI]));
 by (rtac cube 1);
-by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1);
-by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1);
-by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1);
-by (atac 1);
-by (etac (residuals_preserve_comp RS spec RS mp RS mp RS mp) 1);
- by(atac 1);
- by(etac comp_sym 1);
- by(atac 1);
-by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1);
-by (asm_simp_tac prism_ss 1);
-by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1);
-val paving = result();
+by (ALLGOALS (asm_simp_tac (prism_ss addsimps [comp_sym_iff])));
+by (ALLGOALS (blast_tac (!claset addIs [residuals_preserve_comp, 
+					comp_trans, comp_sym])));
+qed "paving";
 

--- a/src/ZF/Resid/Redex.ML	Mon Sep 29 11:51:09 1997 +0200
+++ b/src/ZF/Resid/Redex.ML	Mon Sep 29 11:51:52 1997 +0200
@@ -14,18 +14,18 @@
 goal Redex.thy  "redex_rec(Var(n),b,c,d) = b(n)";
 by (rtac (redex_rec_def RS def_Vrec RS trans) 1);
 by (simp_tac (rank_ss addsimps redexes.con_defs)  1);
-val redex_rec_Var = result();
+qed "redex_rec_Var";
 
 goal Redex.thy  "redex_rec(Fun(t),b,c,d) = c(t,redex_rec(t,b,c,d))";
 by (rtac (redex_rec_def RS def_Vrec RS trans) 1);
 by (simp_tac (rank_ss addsimps redexes.con_defs)  1);
-val redex_rec_Fun = result();
+qed "redex_rec_Fun";
 
 goal Redex.thy  "redex_rec(App(m,f,a),b,c,d) =  \
 \                      d(m,f,a,redex_rec(f,b,c,d),redex_rec(a,b,c,d))";
 by (rtac (redex_rec_def RS def_Vrec RS trans) 1);
 by (simp_tac (rank_ss addsimps redexes.con_defs)  1);
-val redex_rec_App = result();
+qed "redex_rec_App";
 
 Addsimps ([redex_rec_App,redex_rec_Fun,redex_rec_Var]@redexes.intrs);
 

--- 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";
+

--- a/src/ZF/Resid/Residuals.ML	Mon Sep 29 11:51:09 1997 +0200
+++ b/src/ZF/Resid/Residuals.ML	Mon Sep 29 11:51:52 1997 +0200
@@ -47,14 +47,13 @@
     "!!u.residuals(u,v,w) ==> ALL w1.residuals(u,v,w1) --> w1 = w";
 by (etac Sres.induct 1);
 by (ALLGOALS Fast_tac);
-val residuals_function = result();
-val res_is_func  = residuals_function  RS spec RS mp;
+qed_spec_mp "residuals_function";
 
 goal Residuals.thy 
     "!!u.u~v ==> regular(v) --> (EX w.residuals(u,v,w))";
 by (etac Scomp.induct 1);
 by (ALLGOALS Fast_tac);
-val residuals_intro = result();
+qed "residuals_intro";
 
 val prems = goal  Residuals.thy 
     "[|u~v; residuals(u,v,THE w. residuals(u, v, w))==> R; \
@@ -63,38 +62,38 @@
 by (resolve_tac prems 1);
 by (resolve_tac [residuals_intro RS mp RS exE] 1);
 by (resolve_tac [the_equality RS ssubst] 3);
-by (ALLGOALS (fast_tac (!claset addIs [res_is_func])));
-val comp_resfuncE = result();
+by (ALLGOALS (fast_tac (!claset addIs [residuals_function])));
+qed "comp_resfuncE";
 
 
 (* ------------------------------------------------------------------------- *)
 (*               Residual function                                           *)
 (* ------------------------------------------------------------------------- *)
 
-val resfunc_cs = (!claset addIs  [the_equality,res_is_func] 
+val resfunc_cs = (!claset addIs  [the_equality,residuals_function] 
                           addSEs [comp_resfuncE]);
 
 goalw Residuals.thy [res_func_def]
     "!!n.n:nat ==> Var(n) |> Var(n) = Var(n)";
 by (fast_tac resfunc_cs 1);
-val res_Var = result();
+qed "res_Var";
 
 goalw Residuals.thy [res_func_def]
     "!!n.[|s~t; regular(t)|]==> Fun(s) |> Fun(t) = Fun(s |> t)";
 by (fast_tac resfunc_cs 1);
-val res_Fun = result();
+qed "res_Fun";
 
 goalw Residuals.thy [res_func_def]
     "!!n.[|s~u; regular(u); t~v; regular(v); b:bool|]==> \
 \           App(b,s,t) |> App(0,u,v) = App(b, s |> u, t |> v)";
 by (fast_tac resfunc_cs 1);
-val res_App = result();
+qed "res_App";
 
 goalw Residuals.thy [res_func_def]
     "!!n.[|s~u; regular(u); t~v; regular(v); b:bool|]==> \
 \           App(b,Fun(s),t) |> App(1,Fun(u),v) = (t |> v)/ (s |> u)";
 by (fast_tac resfunc_cs 1);
-val res_redex = result();
+qed "res_redex";
 
 goal Residuals.thy
     "!!n.[|s~t; regular(t)|]==> regular(t) --> s |> t:redexes";
@@ -106,7 +105,7 @@
 by (asm_full_simp_tac 
              (!simpset addsimps [res_Fun] 
               setloop (SELECT_GOAL (safe_tac (!claset)))) 1);
-val resfunc_type = result();
+qed "resfunc_type";
 
 Addsimps ([res_Var, res_Fun, res_App, res_redex, lift_rec_preserve_comp,
 	  lift_rec_preserve_reg, subst_rec_preserve_comp, resfunc_type,
@@ -123,42 +122,42 @@
     "!!u.u<==v ==> u~v";
 by (etac Ssub.induct 1);
 by (ALLGOALS Asm_simp_tac);
-val sub_comp = result();
+qed "sub_comp";
 
 goal Residuals.thy 
     "!!u.u<==v  ==> regular(v) --> regular(u)";
 by (etac Ssub.induct 1);
 by (ALLGOALS (asm_simp_tac res1L_ss));
-val sub_preserve_reg = result();
+qed "sub_preserve_reg";
 
 goal Residuals.thy 
     "!!u.[|u~v; k:nat|]==> regular(v)--> (ALL n:nat.  \
 \        lift_rec(u,n) |> lift_rec(v,n) = lift_rec(u |> v,n))";
 by (etac Scomp.induct 1);
-by (Step_tac 1);
+by Safe_tac;
 by (ALLGOALS (asm_full_simp_tac ((addsplit (!simpset)) addsimps [lift_subst])));
 by (dres_inst_tac [("psi", "ALL x:nat.Fun(?u(x)) |> ?v(x) = ?w(x)")] asm_rl 1);
 by (Asm_full_simp_tac 1);
-val residuals_lift_rec = result();
+qed "residuals_lift_rec";
 
 goal Residuals.thy 
     "!!u.u1~u2 ==>  ALL v1 v2.v1~v2 --> regular(v2) --> regular(u2) -->\
 \   (ALL n:nat.subst_rec(v1,u1,n) |> subst_rec(v2,u2,n) = \
 \              subst_rec(v1 |> v2, u1 |> u2,n))";
 by (etac Scomp.induct 1);
-by (Step_tac 1);
+by Safe_tac;
 by (ALLGOALS
     (asm_full_simp_tac ((addsplit (!simpset)) addsimps ([residuals_lift_rec]))));
 by (dres_inst_tac [("psi", "ALL x.?P(x)")] asm_rl 1);
 by (asm_full_simp_tac (!simpset addsimps ([substitution])) 1);
-val residuals_subst_rec = result();
+qed "residuals_subst_rec";
 
 
 goal Residuals.thy 
     "!!u.[|u1~u2; v1~v2; regular(u2); regular(v2)|]==>\
 \       (v1/u1) |> (v2/u2) = (v1 |> v2)/(u1 |> u2)";
 by (asm_simp_tac (!simpset addsimps ([residuals_subst_rec])) 1);
-val commutation = result();
+qed "commutation";
 
 (* ------------------------------------------------------------------------- *)
 (*     Residuals are comp and regular                                        *)
@@ -173,7 +172,7 @@
     THEN resolve_tac Sreg.intrs 3);
 by (REPEAT(assume_tac 1));
 by (asm_full_simp_tac res1L_ss 1);
-val residuals_preserve_comp = result();
+qed_spec_mp "residuals_preserve_comp";
 
 
 goal Residuals.thy 
@@ -182,7 +181,7 @@
 by (safe_tac (!claset));
 by (TRYALL (dres_inst_tac [("psi", "regular(Fun(?u) |> ?v)")] asm_rl));
 by (ALLGOALS (asm_full_simp_tac res1L_ss));
-val residuals_preserve_reg = result();
+qed "residuals_preserve_reg";
 
 (* ------------------------------------------------------------------------- *)
 (*     Preservation lemma                                                    *)
@@ -192,7 +191,7 @@
     "!!u.u~v ==> v ~ (u un v)";
 by (etac Scomp.induct 1);
 by (ALLGOALS Asm_full_simp_tac);
-val union_preserve_comp = result();
+qed "union_preserve_comp";
 
 goal Residuals.thy 
     "!!u.u ~ v ==> regular(v) --> u|>v = (u un v)|>v";
@@ -204,6 +203,4 @@
 by (asm_full_simp_tac (!simpset addsimps 
                        [union_preserve_comp RS comp_sym,
                         comp_sym RS union_preserve_comp RS comp_sym]) 1);
-val preservation1 = result();
-
-val preservation = preservation1 RS mp;
+qed_spec_mp "preservation";

--- a/src/ZF/Resid/SubUnion.ML	Mon Sep 29 11:51:09 1997 +0200
+++ b/src/ZF/Resid/SubUnion.ML	Mon Sep 29 11:51:52 1997 +0200
@@ -25,20 +25,20 @@
     "!!u.n:nat==>Var(n) un Var(n)=Var(n)";
 by (Asm_simp_tac 1);
 by (simp_tac (rank_ss addsimps redexes.con_defs)  1);
-val union_Var = result();
+qed "union_Var";
 
 goalw SubUnion.thy [union_def]
     "!!u.[|u:redexes; v:redexes|]==>Fun(u) un Fun(v)=Fun(u un v)";
 by (Asm_simp_tac 1);
 by (simp_tac (rank_ss addsimps redexes.con_defs)  1);
-val union_Fun = result();
+qed "union_Fun";
  
 goalw SubUnion.thy [union_def]
  "!!u.[|b1:bool; b2:bool; u1:redexes; v1:redexes; u2:redexes; v2:redexes|]==> \
 \     App(b1,u1,v1) un App(b2,u2,v2)=App(b1 or b2,u1 un u2,v1 un v2)";
 by (Asm_simp_tac 1);
 by (simp_tac (rank_ss addsimps redexes.con_defs)  1);
-val union_App = result();
+qed "union_App";
 
 Addsimps (Ssub.intrs@bool_typechecks@
 	  [e-mail]@
@@ -68,27 +68,25 @@
 goal SubUnion.thy "!!u.u:redexes ==> u ~ u";
 by (eresolve_tac [redexes.induct] 1);
 by (ALLGOALS Fast_tac);
-val comp_refl = result();
+qed "comp_refl";
 
 goal SubUnion.thy 
     "!!u.u ~ v ==> v ~ u";
 by (etac Scomp.induct 1);
 by (ALLGOALS Fast_tac);
-val comp_sym = result();
+qed "comp_sym";
 
 goal SubUnion.thy 
     "u ~ v <-> v ~ u";
 by (fast_tac (!claset addIs [comp_sym]) 1);
-val comp_sym_iff = result();
+qed "comp_sym_iff";
 
 
 goal SubUnion.thy 
     "!!u.u ~ v ==> ALL w.v ~ w-->u ~ w";
 by (etac Scomp.induct 1);
 by (ALLGOALS Fast_tac);
-val comp_trans1 = result();
-
-val comp_trans = comp_trans1 RS spec RS mp;
+qed_spec_mp "comp_trans";
 
 (* ------------------------------------------------------------------------- *)
 (*   union proofs                                                            *)
@@ -99,20 +97,20 @@
 by (etac Scomp.induct 1);
 by (etac boolE 3);
 by (ALLGOALS Asm_full_simp_tac);
-val union_l = result();
+qed "union_l";
 
 goal SubUnion.thy 
     "!!u.u ~ v ==> v <== (u un v)";
 by (etac Scomp.induct 1);
 by (eres_inst_tac [("c","b2")] boolE 3);
 by (ALLGOALS Asm_full_simp_tac);
-val union_r = result();
+qed "union_r";
 
 goal SubUnion.thy 
     "!!u.u ~ v ==> u un v = v un u";
 by (etac Scomp.induct 1);
 by (ALLGOALS(asm_simp_tac (!simpset addsimps [or_commute])));
-val union_sym = result();
+qed "union_sym";
 
 (* ------------------------------------------------------------------------- *)
 (*      regular proofs                                                       *)
@@ -125,4 +123,4 @@
              (!simpset setloop(SELECT_GOAL (safe_tac (!claset))))));
 by (dres_inst_tac [("psi", "regular(Fun(?u) un ?v)")] asm_rl 1);
 by (Asm_full_simp_tac 1);
-val union_preserve_regular = result();
+qed_spec_mp "union_preserve_regular";

--- a/src/ZF/Resid/Substitution.ML	Mon Sep 29 11:51:09 1997 +0200
+++ b/src/ZF/Resid/Substitution.ML	Mon Sep 29 11:51:52 1997 +0200
@@ -14,7 +14,7 @@
 goal Arith.thy
     "!!m.[| p < n; n:nat|]==> n~=p";
 by (Fast_tac 1);
-val gt_not_eq = result();
+qed "gt_not_eq";
 
 val succ_pred = prove_goal Arith.thy 
     "!!i.[|j:nat; i:nat|]==> i < j --> succ(j #- 1) = j"
@@ -27,13 +27,13 @@
 by (rtac succ_leE 1);
 by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1);
 by (asm_simp_tac (!simpset addsimps [succ_pred]) 1);
-val lt_pred = result();
+qed "lt_pred";
 
 goal Arith.thy 
     "!!i.[|n < succ(x); p<n; p:nat; n:nat; x:nat|]==> n#-1 < x ";
 by (rtac succ_leE 1);
 by (asm_simp_tac (!simpset addsimps [succ_pred]) 1);
-val gt_pred = result();
+qed "gt_pred";
 
 
 Addsimps [nat_into_Ord, not_lt_iff_le, if_P, if_not_P];
@@ -45,29 +45,29 @@
 goalw Substitution.thy [lift_rec_def] 
     "!!n.[|n:nat; i:nat|]==> lift_rec(Var(i),n) =if(i<n,Var(i),Var(succ(i)))";
 by (Asm_full_simp_tac 1);
-val lift_rec_Var = result();
+qed "lift_rec_Var";
 
 goalw Substitution.thy [lift_rec_def] 
     "!!n.[|n:nat; i:nat; k:nat; k le i|]==> lift_rec(Var(i),k) = Var(succ(i))";
 by (Asm_full_simp_tac 1);
-val lift_rec_le = result();
+qed "lift_rec_le";
 
 goalw Substitution.thy [lift_rec_def] 
     "!!n.[|i:nat; k:nat; i<k |]==> lift_rec(Var(i),k) = Var(i)";
 by (Asm_full_simp_tac 1);
-val lift_rec_gt = result();
+qed "lift_rec_gt";
 
 goalw Substitution.thy [lift_rec_def] 
     "!!n.[|n:nat; k:nat|]==>   \
 \        lift_rec(Fun(t),k) = Fun(lift_rec(t,succ(k)))";
 by (Asm_full_simp_tac 1);
-val lift_rec_Fun = result();
+qed "lift_rec_Fun";
 
 goalw Substitution.thy [lift_rec_def] 
     "!!n.[|n:nat; k:nat|]==>   \
 \        lift_rec(App(b,f,a),k) = App(b,lift_rec(f,k),lift_rec(a,k))";
 by (Asm_full_simp_tac 1);
-val lift_rec_App = result();
+qed "lift_rec_App";
 
 (* ------------------------------------------------------------------------- *)
 (*    substitution quality rules                                             *)
@@ -77,36 +77,36 @@
     "!!n.[|i:nat; k:nat; u:redexes|]==>  \
 \        subst_rec(u,Var(i),k) = if(k<i,Var(i#-1),if(k=i,u,Var(i)))";
 by (asm_full_simp_tac (!simpset addsimps [gt_not_eq,leI]) 1);
-val subst_Var = result();
+qed "subst_Var";
 
 goalw Substitution.thy [subst_rec_def] 
     "!!n.[|n:nat; u:redexes|]==> subst_rec(u,Var(n),n) = u";
 by (asm_full_simp_tac (!simpset) 1);
-val subst_eq = result();
+qed "subst_eq";
 
 goalw Substitution.thy [subst_rec_def] 
     "!!n.[|n:nat; u:redexes; p:nat; p<n|]==>  \
 \        subst_rec(u,Var(n),p) = Var(n#-1)";
 by (asm_full_simp_tac (!simpset) 1);
-val subst_gt = result();
+qed "subst_gt";
 
 goalw Substitution.thy [subst_rec_def] 
     "!!n.[|n:nat; u:redexes; p:nat; n<p|]==>  \
 \        subst_rec(u,Var(n),p) = Var(n)";
 by (asm_full_simp_tac (!simpset addsimps [gt_not_eq,leI]) 1);
-val subst_lt = result();
+qed "subst_lt";
 
 goalw Substitution.thy [subst_rec_def] 
     "!!n.[|p:nat; u:redexes|]==>  \
 \        subst_rec(u,Fun(t),p) = Fun(subst_rec(lift(u),t,succ(p))) ";
 by (asm_full_simp_tac (!simpset) 1);
-val subst_Fun = result();
+qed "subst_Fun";
 
 goalw Substitution.thy [subst_rec_def] 
     "!!n.[|p:nat; u:redexes|]==>  \
 \        subst_rec(u,App(b,f,a),p) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))";
 by (asm_full_simp_tac (!simpset) 1);
-val subst_App = result();
+qed "subst_App";
 
 fun addsplit ss = (ss setloop (split_inside_tac [expand_if]) 
                 addsimps [lift_rec_Var,subst_Var]);
@@ -117,7 +117,7 @@
 by (eresolve_tac [redexes.induct] 1);
 by (ALLGOALS(asm_full_simp_tac 
     ((addsplit (!simpset)) addsimps [lift_rec_Fun,lift_rec_App])));
-val lift_rec_type_a = result();
+qed "lift_rec_type_a";
 val lift_rec_type = lift_rec_type_a RS bspec;
 
 goalw Substitution.thy [] 
@@ -126,7 +126,7 @@
 by (ALLGOALS(asm_full_simp_tac 
     ((addsplit (!simpset)) addsimps [subst_Fun,subst_App,
                        lift_rec_type])));
-val subst_type_a = result();
+qed "subst_type_a";
 val subst_type = subst_type_a RS bspec RS bspec;
 
 
@@ -144,19 +144,19 @@
 \       (lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))";
 by ((eresolve_tac [redexes.induct] 1)
     THEN (ALLGOALS Asm_simp_tac));
-by (step_tac (!claset) 1);
+by Safe_tac;
 by (excluded_middle_tac "na < xa" 1);
 by ((forward_tac [lt_trans2] 2) THEN (assume_tac 2));
 by (ALLGOALS(asm_full_simp_tac 
     ((addsplit (!simpset)) addsimps [leI])));
-val lift_lift_rec = result();
+qed "lift_lift_rec";
 
 
 goalw Substitution.thy [] 
     "!!n.[|u:redexes; n:nat|]==>  \
 \      lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))";
 by (asm_simp_tac (!simpset addsimps [lift_lift_rec]) 1);
-val lift_lift = result();
+qed "lift_lift";
 
 goal Substitution.thy 
     "!!n.v:redexes ==>  \
@@ -165,7 +165,7 @@
 \              subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)";
 by ((eresolve_tac [redexes.induct] 1)
     THEN (ALLGOALS(asm_simp_tac (!simpset addsimps [lift_lift]))));
-by (step_tac (!claset) 1);
+by Safe_tac;
 by (excluded_middle_tac "na < x" 1);
 by (asm_full_simp_tac (!simpset) 1);
 by (eres_inst_tac [("j","na")] leE 1);
@@ -176,13 +176,13 @@
 by (forw_inst_tac [("j","x")] lt_trans2 1);
 by (assume_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [leI]) 1);
-val lift_rec_subst_rec = result();
+qed "lift_rec_subst_rec";
 
 goalw Substitution.thy [] 
     "!!n.[|v:redexes; u:redexes; n:nat|]==>  \
 \        lift_rec(u/v,n) = lift_rec(u,n)/lift_rec(v,succ(n))";
 by (asm_full_simp_tac (!simpset addsimps [lift_rec_subst_rec]) 1);
-val lift_subst = result();
+qed "lift_subst";
 
 
 goalw Substitution.thy [] 
@@ -192,7 +192,7 @@
 \              subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))";
 by ((eresolve_tac [redexes.induct] 1)
     THEN (ALLGOALS(asm_simp_tac (!simpset addsimps [lift_lift]))));
-by (step_tac (!claset) 1);
+by Safe_tac;
 by (excluded_middle_tac "na < x" 1);
 by (asm_full_simp_tac (!simpset) 1);
 by (eres_inst_tac [("i","x")] leE 1);
@@ -204,7 +204,7 @@
 by (excluded_middle_tac "na < xa" 1);
 by (asm_full_simp_tac (!simpset) 1);
 by (asm_full_simp_tac (!simpset addsimps [leI]) 1);
-val lift_rec_subst_rec_lt = result();
+qed "lift_rec_subst_rec_lt";
 
 
 goalw Substitution.thy [] 
@@ -212,12 +212,12 @@
 \       ALL n:nat.ALL v:redexes.subst_rec(v,lift_rec(u,n),n) =  u";
 by ((eresolve_tac [redexes.induct] 1)
     THEN (ALLGOALS Asm_simp_tac));
-by (step_tac (!claset) 1);
+by Safe_tac;
 by (excluded_middle_tac "na < x" 1);
 (* x <= na  *)
 by (asm_full_simp_tac (!simpset) 1);
 by (asm_full_simp_tac (!simpset) 1);
-val subst_rec_lift_rec = result();
+qed "subst_rec_lift_rec";
 
 goal Substitution.thy  
     "!!n.v:redexes ==>  \
@@ -227,7 +227,7 @@
 by ((eresolve_tac [redexes.induct] 1) THEN 
      (ALLGOALS(asm_simp_tac (!simpset addsimps 
                              [lift_lift RS sym,lift_rec_subst_rec_lt]))));
-by (step_tac (!claset) 1);
+by Safe_tac;
 by (excluded_middle_tac "na  le succ(xa)" 1);
 by (asm_full_simp_tac (!simpset) 1);
 by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1);
@@ -247,14 +247,14 @@
 by (asm_simp_tac (!simpset addsimps [subst_rec_lift_rec]) 1);
 by (forward_tac [lt_trans2] 1 THEN assume_tac 1);
 by (asm_simp_tac (!simpset addsimps [gt_pred]) 1);
-val subst_rec_subst_rec = result();
+qed "subst_rec_subst_rec";
 
 
 goalw Substitution.thy [] 
     "!!n.[|v:redexes; u:redexes; w:redexes; n:nat|]==>  \
 \       subst_rec(w,u,n)/subst_rec(lift(w),v,succ(n)) = subst_rec(w,u/v,n)";
 by (asm_simp_tac (!simpset addsimps [subst_rec_subst_rec]) 1);
-val substitution = result();
+qed "substitution";
 
 (* ------------------------------------------------------------------------- *)
 (*          Preservation lemmas                                              *)
@@ -266,7 +266,7 @@
     "!!n.[|n:nat; u ~ v|]==> ALL m:nat.lift_rec(u,m) ~ lift_rec(v,m)";
 by (etac Scomp.induct 1);
 by (ALLGOALS(asm_simp_tac (!simpset addsimps [comp_refl])));
-val lift_rec_preserve_comp = result();
+qed "lift_rec_preserve_comp";
 
 goal Substitution.thy
     "!!n.u2 ~ v2 ==> ALL m:nat.ALL u1:redexes.ALL v1:redexes.\
@@ -274,13 +274,13 @@
 by (etac Scomp.induct 1);
 by (ALLGOALS(asm_full_simp_tac ((addsplit (!simpset)) addsimps 
             ([lift_rec_preserve_comp,comp_refl]))));
-val subst_rec_preserve_comp = result();
+qed "subst_rec_preserve_comp";
 
 goal Substitution.thy
     "!!n.regular(u) ==> ALL m:nat.regular(lift_rec(u,m))";
 by (eresolve_tac [Sreg.induct] 1);
 by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset))));
-val lift_rec_preserve_reg = result();
+qed "lift_rec_preserve_reg";
 
 goal Substitution.thy
     "!!n.regular(v) ==>  \
@@ -288,4 +288,4 @@
 by (eresolve_tac [Sreg.induct] 1);
 by (ALLGOALS(asm_full_simp_tac ((addsplit (!simpset)) addsimps 
             [lift_rec_preserve_reg])));
-val subst_rec_preserve_reg = result();
+qed "subst_rec_preserve_reg";

--- a/src/ZF/Resid/Terms.ML	Mon Sep 29 11:51:09 1997 +0200
+++ b/src/ZF/Resid/Terms.ML	Mon Sep 29 11:51:52 1997 +0200
@@ -14,17 +14,17 @@
 goalw Terms.thy [unmark_def] 
     "unmark(Var(n)) = Var(n)";
 by (Asm_simp_tac 1);
-val unmark_Var = result();
+qed "unmark_Var";
 
 goalw Terms.thy [unmark_def] 
     "unmark(Fun(t)) = Fun(unmark(t))";
 by (Asm_simp_tac 1);
-val unmark_Fun = result();
+qed "unmark_Fun";
 
 goalw Terms.thy [unmark_def] 
     "unmark(App(b,n,m)) = App(0,unmark(n),unmark(m))";
 by (Asm_simp_tac 1);
-val unmark_App = result();
+qed "unmark_App";
 
 
 (* ------------------------------------------------------------------------- *)
@@ -45,13 +45,13 @@
     "!!u.u:redexes ==> unmark(u):lambda";
 by (eresolve_tac [redexes.induct] 1);
 by (ALLGOALS Asm_simp_tac);
-val unmark_type = result();
+qed "unmark_type";
 
 goal Terms.thy  
     "!!u.u:lambda ==> unmark(u) = u";
 by (eresolve_tac [lambda.induct] 1);
 by (ALLGOALS Asm_simp_tac);
-val lambda_unmark = result();
+qed "lambda_unmark";
 
 
 (* ------------------------------------------------------------------------- *)
@@ -62,14 +62,14 @@
     "!!u.[|v:lambda|]==> ALL k:nat.lift_rec(v,k):lambda";
 by (eresolve_tac [lambda.induct] 1);
 by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset))));
-val liftL_typea = result();
+qed "liftL_typea";
 val liftL_type =liftL_typea RS bspec ;
 
 goal Terms.thy  
     "!!n.[|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])));
-val substL_typea = result();
+qed "substL_typea";
 val substL_type = substL_typea RS bspec RS bspec ;