# HG changeset patch
# User clasohm
# Date 786200026 -3600
# Node ID 2ca12511676dbd2db99ab0a2cba10a477071e83c
# Parent  e0e5c1581e4c47a289567ed2cbe6622b024546f9
added qed and qed_goal[w]

diff -r e0e5c1581e4c -r 2ca12511676d src/CCL/CCL.ML
--- a/src/CCL/CCL.ML	Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/CCL.ML	Wed Nov 30 13:53:46 1994 +0100
@@ -16,17 +16,17 @@
 (*** Congruence Rules ***)
 
 (*similar to AP_THM in Gordon's HOL*)
-val fun_cong = prove_goal CCL.thy "(f::'a=>'b) = g ==> f(x)=g(x)"
+qed_goal "fun_cong" CCL.thy "(f::'a=>'b) = g ==> f(x)=g(x)"
   (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
 
 (*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
-val arg_cong = prove_goal CCL.thy "x=y ==> f(x)=f(y)"
+qed_goal "arg_cong" CCL.thy "x=y ==> f(x)=f(y)"
  (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
 
 goal CCL.thy  "(ALL x. f(x) = g(x)) --> (%x.f(x)) = (%x.g(x))";
 by (simp_tac (CCL_ss addsimps [eq_iff]) 1);
 by (fast_tac (set_cs addIs [po_abstractn]) 1);
-val abstractn = standard (allI RS (result() RS mp));
+val abstractn = store_thm("abstractn", standard (allI RS (result() RS mp)));
 
 fun type_of_terms (Const("Trueprop",_) $ 
                    (Const("op =",(Type ("fun", [t,_]))) $ _ $ _)) = t;
@@ -45,18 +45,18 @@
 
 goalw CCL.thy [Trm_def,Dvg_def] "Trm(t) <-> ~ t = bot";
 by (rtac iff_refl 1);
-val Trm_iff = result();
+qed "Trm_iff";
 
 goalw CCL.thy [Trm_def,Dvg_def] "Dvg(t) <-> t = bot";
 by (rtac iff_refl 1);
-val Dvg_iff = result();
+qed "Dvg_iff";
 
 (*** Constructors are injective ***)
 
 val prems = goal CCL.thy
     "[| x=a;  y=b;  x=y |] ==> a=b";
 by  (REPEAT (SOMEGOAL (ares_tac (prems@[box_equals]))));
-val eq_lemma = result();
+qed "eq_lemma";
 
 fun mk_inj_rl thy rews s = 
       let fun mk_inj_lemmas r = ([arg_cong] RL [(r RS (r RS eq_lemma))]);
@@ -139,11 +139,11 @@
 
 val major::prems = goal Set.thy "[| A=B;  a:B <-> P |] ==> a:A <-> P";
 by (resolve_tac (prems RL [major RS ssubst]) 1);
-val XHlemma1 = result();
+qed "XHlemma1";
 
 goal CCL.thy "(P(t,t') <-> Q) --> (<t,t'> : {p.EX t t'.p=<t,t'> &  P(t,t')} <-> Q)";
 by (fast_tac ccl_cs 1);
-val XHlemma2 = result() RS mp;
+val XHlemma2 = store_thm("XHlemma2", result() RS mp);
 
 (*** Pre-Order ***)
 
@@ -153,14 +153,14 @@
 by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
 by (ALLGOALS (simp_tac ccl_ss));
 by (ALLGOALS (fast_tac set_cs));
-val POgen_mono = result();
+qed "POgen_mono";
 
 goalw CCL.thy [POgen_def,SIM_def]
   "<t,t'> : POgen(R) <-> t= bot | (t=true & t'=true)  | (t=false & t'=false) | \
 \                    (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
 \                    (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))";
 by (rtac (iff_refl RS XHlemma2) 1);
-val POgenXH = result();
+qed "POgenXH";
 
 goal CCL.thy
   "t [= t' <-> t=bot | (t=true & t'=true) | (t=false & t'=false) | \
@@ -170,25 +170,25 @@
 br (rewrite_rule [POgen_def,SIM_def] 
                  (POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1;
 by (rtac (iff_refl RS XHlemma2) 1);
-val poXH = result();
+qed "poXH";
 
 goal CCL.thy "bot [= b";
 by (rtac (poXH RS iffD2) 1);
 by (simp_tac ccl_ss 1);
-val po_bot = result();
+qed "po_bot";
 
 goal CCL.thy "a [= bot --> a=bot";
 by (rtac impI 1);
 by (dtac (poXH RS iffD1) 1);
 by (etac rev_mp 1);
 by (simp_tac ccl_ss 1);
-val bot_poleast = result() RS mp;
+val bot_poleast = store_thm("bot_poleast", result() RS mp);
 
 goal CCL.thy "<a,b> [= <a',b'> <->  a [= a' & b [= b'";
 by (rtac (poXH RS iff_trans) 1);
 by (simp_tac ccl_ss 1);
 by (fast_tac ccl_cs 1);
-val po_pair = result();
+qed "po_pair";
 
 goal CCL.thy "lam x.f(x) [= lam x.f'(x) <-> (ALL x. f(x) [= f'(x))";
 by (rtac (poXH RS iff_trans) 1);
@@ -196,7 +196,7 @@
 by (REPEAT (ares_tac [iffI,allI] 1 ORELSE eresolve_tac [exE,conjE] 1));
 by (asm_simp_tac ccl_ss 1);
 by (fast_tac ccl_cs 1);
-val po_lam = result();
+qed "po_lam";
 
 val ccl_porews = [po_bot,po_pair,po_lam];
 
@@ -210,40 +210,40 @@
 by (res_inst_tac [("f1","%d.case(t',a',b',c',d)")] 
                (p5 RS po_abstractn RS po_cong RS po_trans) 1);
 by (rtac po_refl 1);
-val case_pocong = result();
+qed "case_pocong";
 
 val [p1,p2] = goalw CCL.thy ccl_data_defs
     "[| f [= f';  a [= a' |] ==> f ` a [= f' ` a'";
 by (REPEAT (ares_tac [po_refl,case_pocong,p1,p2 RS po_cong] 1));
-val apply_pocong = result();
+qed "apply_pocong";
 
 
 val prems = goal CCL.thy "~ lam x.b(x) [= bot";
 by (rtac notI 1);
 by (dtac bot_poleast 1);
 by (etac (distinctness RS notE) 1);
-val npo_lam_bot = result();
+qed "npo_lam_bot";
 
 val eq1::eq2::prems = goal CCL.thy
     "[| x=a;  y=b;  x[=y |] ==> a[=b";
 by (rtac (eq1 RS subst) 1);
 by (rtac (eq2 RS subst) 1);
 by (resolve_tac prems 1);
-val po_lemma = result();
+qed "po_lemma";
 
 goal CCL.thy "~ <a,b> [= lam x.f(x)";
 by (rtac notI 1);
 by (rtac (npo_lam_bot RS notE) 1);
 by (etac (case_pocong RS (caseBlam RS (caseBpair RS po_lemma))) 1);
 by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1));
-val npo_pair_lam = result();
+qed "npo_pair_lam";
 
 goal CCL.thy "~ lam x.f(x) [= <a,b>";
 by (rtac notI 1);
 by (rtac (npo_lam_bot RS notE) 1);
 by (etac (case_pocong RS (caseBpair RS (caseBlam RS po_lemma))) 1);
 by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1));
-val npo_lam_pair = result();
+qed "npo_lam_pair";
 
 fun mk_thm s = prove_goal CCL.thy s (fn _ => 
                           [rtac notI 1,dtac case_pocong 1,etac rev_mp 5,
@@ -262,7 +262,7 @@
 val prems = goal CCL.thy "[|  <t,u> : R;  R <= POgen(R) |] ==> t [= u";
 by (rtac (PO_def RS def_coinduct RS (PO_iff RS iffD2)) 1);
 by (REPEAT (ares_tac prems 1));
-val po_coinduct = result();
+qed "po_coinduct";
 
 fun po_coinduct_tac s i = res_inst_tac [("R",s)] po_coinduct i;
 
@@ -274,7 +274,7 @@
 by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
 by (ALLGOALS (simp_tac ccl_ss));
 by (ALLGOALS (fast_tac set_cs));
-val EQgen_mono = result();
+qed "EQgen_mono";
 
 goalw CCL.thy [EQgen_def,SIM_def]
   "<t,t'> : EQgen(R) <-> (t=bot & t'=bot)  | (t=true & t'=true)  | \
@@ -282,7 +282,7 @@
 \                (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
 \                (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))";
 by (rtac (iff_refl RS XHlemma2) 1);
-val EQgenXH = result();
+qed "EQgenXH";
 
 goal CCL.thy
   "t=t' <-> (t=bot & t'=bot)  | (t=true & t'=true)  | (t=false & t'=false) | \
@@ -297,18 +297,18 @@
 br (rewrite_rule [EQgen_def,SIM_def]
                  (EQgen_mono RS (EQ_def RS def_gfp_Tarski) RS XHlemma1)) 1;
 by (rtac (iff_refl RS XHlemma2) 1);
-val eqXH = result();
+qed "eqXH";
 
 val prems = goal CCL.thy "[|  <t,u> : R;  R <= EQgen(R) |] ==> t = u";
 by (rtac (EQ_def RS def_coinduct RS (EQ_iff RS iffD2)) 1);
 by (REPEAT (ares_tac prems 1));
-val eq_coinduct = result();
+qed "eq_coinduct";
 
 val prems = goal CCL.thy 
     "[|  <t,u> : R;  R <= EQgen(lfp(%x.EQgen(x) Un R Un EQ)) |] ==> t = u";
 by (rtac (EQ_def RS def_coinduct3 RS (EQ_iff RS iffD2)) 1);
 by (REPEAT (ares_tac (EQgen_mono::prems) 1));
-val eq_coinduct3 = result();
+qed "eq_coinduct3";
 
 fun eq_coinduct_tac s i = res_inst_tac [("R",s)] eq_coinduct i;
 fun eq_coinduct3_tac s i = res_inst_tac [("R",s)] eq_coinduct3 i;
@@ -318,17 +318,17 @@
 goalw CCL.thy [apply_def]  "(EX f.t=lam x.f(x)) --> t = lam x.(t ` x)";
 by (safe_tac ccl_cs);
 by (simp_tac ccl_ss 1);
-val cond_eta = result() RS mp;
+val cond_eta = store_thm("cond_eta", result() RS mp);
 
 goal CCL.thy "(t=bot) | (t=true) | (t=false) | (EX a b.t=<a,b>) | (EX f.t=lam x.f(x))";
 by (cut_facts_tac [refl RS (eqXH RS iffD1)] 1);
 by (fast_tac set_cs 1);
-val exhaustion = result();
+qed "exhaustion";
 
 val prems = goal CCL.thy 
     "[| P(bot);  P(true);  P(false);  !!x y.P(<x,y>);  !!b.P(lam x.b(x)) |] ==> P(t)";
 by (cut_facts_tac [exhaustion] 1);
 by (REPEAT_SOME (ares_tac prems ORELSE' eresolve_tac [disjE,exE,ssubst]));
-val term_case = result();
+qed "term_case";
 
 fun term_case_tac a i = res_inst_tac [("t",a)] term_case i;
diff -r e0e5c1581e4c -r 2ca12511676d src/CCL/Fix.ML
--- a/src/CCL/Fix.ML	Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/Fix.ML	Wed Nov 30 13:53:46 1994 +0100
@@ -16,30 +16,30 @@
 by (rtac (Nat_ind RS ballI) 1 THEN atac 1);
 by (ALLGOALS (simp_tac term_ss));
 by (REPEAT (ares_tac [base,step] 1));
-val fix_ind = result();
+qed "fix_ind";
 
 (*** Inclusive Predicates ***)
 
 val prems = goalw Fix.thy [INCL_def]
      "INCL(P) <-> (ALL f. (ALL n:Nat. P(f ^ n ` bot)) --> P(fix(f)))";
 by (rtac iff_refl 1);
-val inclXH = result();
+qed "inclXH";
 
 val prems = goal Fix.thy
      "[| !!f.ALL n:Nat.P(f^n`bot) ==> P(fix(f)) |] ==> INCL(%x.P(x))";
 by (fast_tac (term_cs addIs (prems @ [XH_to_I inclXH])) 1);
-val inclI = result();
+qed "inclI";
 
 val incl::prems = goal Fix.thy
      "[| INCL(P);  !!n.n:Nat ==> P(f^n`bot) |] ==> P(fix(f))";
 by (fast_tac (term_cs addIs ([ballI RS (incl RS (XH_to_D inclXH) RS spec RS mp)] 
                        @ prems)) 1);
-val inclD = result();
+qed "inclD";
 
 val incl::prems = goal Fix.thy
      "[| INCL(P);  (ALL n:Nat.P(f^n`bot))-->P(fix(f)) ==> R |] ==> R";
 by (fast_tac (term_cs addIs ([incl RS inclD] @ prems)) 1);
-val inclE = result();
+qed "inclE";
 
 
 (*** Lemmas for Inclusive Predicates ***)
@@ -53,24 +53,24 @@
 by (assume_tac 2);
 by (rtac (napplyBzero RS ssubst) 1);
 by (rtac po_cong 1 THEN rtac po_bot 1);
-val npo_INCL = result();
+qed "npo_INCL";
 
 val prems = goal Fix.thy "[| INCL(P);  INCL(Q) |] ==> INCL(%x.P(x) & Q(x))";
 by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
-val conj_INCL = result();
+qed "conj_INCL";
 
 val prems = goal Fix.thy "[| !!a.INCL(P(a)) |] ==> INCL(%x.ALL a.P(a,x))";
 by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
-val all_INCL = result();
+qed "all_INCL";
 
 val prems = goal Fix.thy "[| !!a.a:A ==> INCL(P(a)) |] ==> INCL(%x.ALL a:A.P(a,x))";
 by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
-val ball_INCL = result();
+qed "ball_INCL";
 
 goal Fix.thy "INCL(%x.a(x) = (b(x)::'a::prog))";
 by (simp_tac (term_ss addsimps [eq_iff]) 1);
 by (REPEAT (resolve_tac [conj_INCL,po_INCL] 1));
-val eq_INCL = result();
+qed "eq_INCL";
 
 (*** Derivation of Reachability Condition ***)
 
@@ -78,13 +78,13 @@
 
 goal Fix.thy "idgen(fix(idgen)) = fix(idgen)";
 by (rtac (fixB RS sym) 1);
-val fix_idgenfp = result();
+qed "fix_idgenfp";
 
 goalw Fix.thy [idgen_def] "idgen(lam x.x) = lam x.x";
 by (simp_tac term_ss 1);
 by (rtac (term_case RS allI) 1);
 by (ALLGOALS (simp_tac term_ss));
-val id_idgenfp = result();
+qed "id_idgenfp";
 
 (* All fixed points are lam-expressions *)
 
@@ -92,14 +92,14 @@
 by (rtac (prem RS subst) 1);
 by (rewtac idgen_def);
 by (rtac refl 1);
-val idgenfp_lam = result();
+qed "idgenfp_lam";
 
 (* Lemmas for rewriting fixed points of idgen *)
 
 val prems = goalw Fix.thy [idgen_def] 
     "[| a = b;  a ` t = u |] ==> b ` t = u";
 by (simp_tac (term_ss addsimps (prems RL [sym])) 1);
-val l_lemma= result();
+qed "l_lemma";
 
 val idgen_lemmas =
     let fun mk_thm s = prove_goalw Fix.thy [idgen_def] s
@@ -120,12 +120,12 @@
 by (rtac (p2 RS cond_eta RS ssubst) 1);
 by (rtac (p3 RS cond_eta RS ssubst) 1);
 by (rtac (p1 RS (po_lam RS iffD2)) 1);
-val po_eta = result();
+qed "po_eta";
 
 val [prem] = goalw Fix.thy [idgen_def] "idgen(d) = d ==> d = lam x.?f(x)";
 by (rtac (prem RS subst) 1);
 by (rtac refl 1);
-val po_eta_lemma = result();
+qed "po_eta_lemma";
 
 val [prem] = goal Fix.thy
     "idgen(d) = d ==> \
@@ -135,14 +135,14 @@
 by (term_case_tac "t" 1);
 by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem,fix_idgenfp] RL idgen_lemmas)))));
 by (ALLGOALS (fast_tac set_cs));
-val lemma1 = result();
+qed "lemma1";
 
 val [prem] = goal Fix.thy
     "idgen(d) = d ==> fix(idgen) [= d";
 by (rtac (allI RS po_eta) 1);
 by (rtac (lemma1 RSN(2,po_coinduct)) 1);
 by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp])));
-val fix_least_idgen = result();
+qed "fix_least_idgen";
 
 val [prem] = goal Fix.thy
     "idgen(d) = d ==> \
@@ -151,7 +151,7 @@
 by (term_case_tac "a" 1);
 by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem] RL idgen_lemmas)))));
 by (ALLGOALS (fast_tac set_cs));
-val lemma2 = result();
+qed "lemma2";
 
 val [prem] = goal Fix.thy
     "idgen(d) = d ==> lam x.x [= d";
@@ -159,20 +159,20 @@
 by (rtac (lemma2 RSN(2,po_coinduct)) 1);
 by (simp_tac term_ss 1);
 by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp])));
-val id_least_idgen = result();
+qed "id_least_idgen";
 
 goal Fix.thy  "fix(idgen) = lam x.x";
 by (fast_tac (term_cs addIs [eq_iff RS iffD2,
                              id_idgenfp RS fix_least_idgen,
                              fix_idgenfp RS id_least_idgen]) 1);
-val reachability = result();
+qed "reachability";
 
 (********)
 
 val [prem] = goal Fix.thy "f = lam x.x ==> f`t = t";
 by (rtac (prem RS sym RS subst) 1);
 by (rtac applyB 1);
-val id_apply = result();
+qed "id_apply";
 
 val prems = goal Fix.thy
      "[| P(bot);  P(true);  P(false);  \
@@ -190,5 +190,5 @@
 by (res_inst_tac [("t","xa")] term_case 1);
 by (ALLGOALS (simp_tac term_ss));
 by (ALLGOALS (fast_tac (term_cs addIs ([all_INCL,INCL_subst] @ prems))));
-val term_ind = result();
+qed "term_ind";
 
diff -r e0e5c1581e4c -r 2ca12511676d src/CCL/Gfp.ML
--- a/src/CCL/Gfp.ML	Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/Gfp.ML	Wed Nov 30 13:53:46 1994 +0100
@@ -18,27 +18,27 @@
 val prems = goalw Gfp.thy [gfp_def] "[| A <= f(A) |] ==> A <= gfp(f)";
 by (rtac (CollectI RS Union_upper) 1);
 by (resolve_tac prems 1);
-val gfp_upperbound = result();
+qed "gfp_upperbound";
 
 val prems = goalw Gfp.thy [gfp_def]
     "[| !!u. u <= f(u) ==> u<=A |] ==> gfp(f) <= A";
 by (REPEAT (ares_tac ([Union_least]@prems) 1));
 by (etac CollectD 1);
-val gfp_least = result();
+qed "gfp_least";
 
 val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) <= f(gfp(f))";
 by (EVERY1 [rtac gfp_least, rtac subset_trans, atac,
 	    rtac (mono RS monoD), rtac gfp_upperbound, atac]);
-val gfp_lemma2 = result();
+qed "gfp_lemma2";
 
 val [mono] = goal Gfp.thy "mono(f) ==> f(gfp(f)) <= gfp(f)";
 by (EVERY1 [rtac gfp_upperbound, rtac (mono RS monoD), 
 	    rtac gfp_lemma2, rtac mono]);
-val gfp_lemma3 = result();
+qed "gfp_lemma3";
 
 val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) = f(gfp(f))";
 by (REPEAT (resolve_tac [equalityI,gfp_lemma2,gfp_lemma3,mono] 1));
-val gfp_Tarski = result();
+qed "gfp_Tarski";
 
 (*** Coinduction rules for greatest fixed points ***)
 
@@ -47,7 +47,7 @@
     "[| a: A;  A <= f(A) |] ==> a : gfp(f)";
 by (rtac (gfp_upperbound RS subsetD) 1);
 by (REPEAT (ares_tac prems 1));
-val coinduct = result();
+qed "coinduct";
 
 val [prem,mono] = goal Gfp.thy
     "[| A <= f(A) Un gfp(f);  mono(f) |] ==>  \
@@ -57,7 +57,7 @@
 by (rtac (mono RS gfp_Tarski RS subst) 1);
 by (rtac (prem RS Un_least) 1);
 by (rtac Un_upper2 1);
-val coinduct2_lemma = result();
+qed "coinduct2_lemma";
 
 (*strong version, thanks to Martin Coen*)
 val ainA::prems = goal Gfp.thy
@@ -65,7 +65,7 @@
 by (rtac coinduct 1);
 by (rtac (prems MRS coinduct2_lemma) 2);
 by (resolve_tac [ainA RS UnI1] 1);
-val coinduct2 = result();
+qed "coinduct2";
 
 (***  Even Stronger version of coinduct  [by Martin Coen]
          - instead of the condition  A <= f(A)
@@ -73,7 +73,7 @@
 
 val [prem] = goal Gfp.thy "mono(f) ==> mono(%x.f(x) Un A Un B)";
 by (REPEAT (ares_tac [subset_refl, monoI, Un_mono, prem RS monoD] 1));
-val coinduct3_mono_lemma= result();
+qed "coinduct3_mono_lemma";
 
 val [prem,mono] = goal Gfp.thy
     "[| A <= f(lfp(%x.f(x) Un A Un gfp(f)));  mono(f) |] ==> \
@@ -87,7 +87,7 @@
 by (rtac (mono RS monoD) 1);
 by (rtac (mono RS coinduct3_mono_lemma RS lfp_Tarski RS ssubst) 1);
 by (rtac Un_upper2 1);
-val coinduct3_lemma = result();
+qed "coinduct3_lemma";
 
 val ainA::prems = goal Gfp.thy
     "[| a:A;  A <= f(lfp(%x.f(x) Un A Un gfp(f))); mono(f) |] ==> a : gfp(f)";
@@ -95,7 +95,7 @@
 by (rtac (prems MRS coinduct3_lemma) 2);
 by (resolve_tac (prems RL [coinduct3_mono_lemma RS lfp_Tarski RS ssubst]) 1);
 by (rtac (ainA RS UnI2 RS UnI1) 1);
-val coinduct3 = result();
+qed "coinduct3";
 
 
 (** Definition forms of gfp_Tarski, to control unfolding **)
@@ -103,25 +103,25 @@
 val [rew,mono] = goal Gfp.thy "[| h==gfp(f);  mono(f) |] ==> h = f(h)";
 by (rewtac rew);
 by (rtac (mono RS gfp_Tarski) 1);
-val def_gfp_Tarski = result();
+qed "def_gfp_Tarski";
 
 val rew::prems = goal Gfp.thy
     "[| h==gfp(f);  a:A;  A <= f(A) |] ==> a: h";
 by (rewtac rew);
 by (REPEAT (ares_tac (prems @ [coinduct]) 1));
-val def_coinduct = result();
+qed "def_coinduct";
 
 val rew::prems = goal Gfp.thy
     "[| h==gfp(f);  a:A;  A <= f(A) Un h; mono(f) |] ==> a: h";
 by (rewtac rew);
 by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct2]) 1));
-val def_coinduct2 = result();
+qed "def_coinduct2";
 
 val rew::prems = goal Gfp.thy
     "[| h==gfp(f);  a:A;  A <= f(lfp(%x.f(x) Un A Un h)); mono(f) |] ==> a: h";
 by (rewtac rew);
 by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct3]) 1));
-val def_coinduct3 = result();
+qed "def_coinduct3";
 
 (*Monotonicity of gfp!*)
 val prems = goal Gfp.thy
@@ -131,4 +131,4 @@
 by (rtac gfp_lemma2 1);
 by (resolve_tac prems 1);
 by (resolve_tac prems 1);
-val gfp_mono = result();
+qed "gfp_mono";
diff -r e0e5c1581e4c -r 2ca12511676d src/CCL/Hered.ML
--- a/src/CCL/Hered.ML	Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/Hered.ML	Wed Nov 30 13:53:46 1994 +0100
@@ -15,13 +15,13 @@
 goalw Hered.thy [HTTgen_def]  "mono(%X.HTTgen(X))";
 by (rtac monoI 1);
 by (fast_tac set_cs 1);
-val HTTgen_mono = result();
+qed "HTTgen_mono";
 
 goalw Hered.thy [HTTgen_def]
   "t : HTTgen(A) <-> t=true | t=false | (EX a b.t=<a,b> & a : A & b : A) | \
 \                                       (EX f.t=lam x.f(x) & (ALL x.f(x) : A))";
 by (fast_tac set_cs 1);
-val HTTgenXH = result();
+qed "HTTgenXH";
 
 goal Hered.thy
   "t : HTT <-> t=true | t=false | (EX a b.t=<a,b> & a : HTT & b : HTT) | \
@@ -29,26 +29,26 @@
 br (rewrite_rule [HTTgen_def] 
                  (HTTgen_mono RS (HTT_def RS def_gfp_Tarski) RS XHlemma1)) 1;
 by (fast_tac set_cs 1);
-val HTTXH = result();
+qed "HTTXH";
 
 (*** Introduction Rules for HTT ***)
 
 goal Hered.thy "~ bot : HTT";
 by (fast_tac (term_cs addDs [XH_to_D HTTXH]) 1);
-val HTT_bot = result();
+qed "HTT_bot";
 
 goal Hered.thy "true : HTT";
 by (fast_tac (term_cs addIs [XH_to_I HTTXH]) 1);
-val HTT_true = result();
+qed "HTT_true";
 
 goal Hered.thy "false : HTT";
 by (fast_tac (term_cs addIs [XH_to_I HTTXH]) 1);
-val HTT_false = result();
+qed "HTT_false";
 
 goal Hered.thy "<a,b> : HTT <->  a : HTT  & b : HTT";
 by (rtac (HTTXH RS iff_trans) 1);
 by (fast_tac term_cs 1);
-val HTT_pair = result();
+qed "HTT_pair";
 
 goal Hered.thy "lam x.f(x) : HTT <-> (ALL x. f(x) : HTT)";
 by (rtac (HTTXH RS iff_trans) 1);
@@ -56,7 +56,7 @@
 by (safe_tac term_cs);
 by (asm_simp_tac term_ss 1);
 by (fast_tac term_cs 1);
-val HTT_lam = result();
+qed "HTT_lam";
 
 local
   val raw_HTTrews = [HTT_bot,HTT_true,HTT_false,HTT_pair,HTT_lam];
@@ -80,7 +80,7 @@
 val prems = goal Hered.thy "[|  t : R;  R <= HTTgen(R) |] ==> t : HTT";
 by (rtac (HTT_def RS def_coinduct) 1);
 by (REPEAT (ares_tac prems 1));
-val HTT_coinduct = result();
+qed "HTT_coinduct";
 
 fun HTT_coinduct_tac s i = res_inst_tac [("R",s)] HTT_coinduct i;
 
@@ -88,7 +88,7 @@
     "[|  t : R;   R <= HTTgen(lfp(%x. HTTgen(x) Un R Un HTT)) |] ==> t : HTT";
 by (rtac (HTTgen_mono RSN(3,HTT_def RS def_coinduct3)) 1);
 by (REPEAT (ares_tac prems 1));
-val HTT_coinduct3 = result();
+qed "HTT_coinduct3";
 val HTT_coinduct3_raw = rewrite_rule [HTTgen_def] HTT_coinduct3;
 
 fun HTT_coinduct3_tac s i = res_inst_tac [("R",s)] HTT_coinduct3 i;
@@ -114,23 +114,23 @@
 
 goal Hered.thy "Unit <= HTT";
 by (simp_tac (CCL_ss addsimps ([subsetXH,UnitXH] @ HTT_rews)) 1);
-val UnitF = result();
+qed "UnitF";
 
 goal Hered.thy "Bool <= HTT";
 by (simp_tac (CCL_ss addsimps ([subsetXH,BoolXH] @ HTT_rews)) 1);
 by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
-val BoolF = result();
+qed "BoolF";
 
 val prems = goal Hered.thy "[| A <= HTT;  B <= HTT |] ==> A + B  <= HTT";
 by (simp_tac (CCL_ss addsimps ([subsetXH,PlusXH] @ HTT_rews)) 1);
 by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
-val PlusF = result();
+qed "PlusF";
 
 val prems = goal Hered.thy 
      "[| A <= HTT;  !!x.x:A ==> B(x) <= HTT |] ==> SUM x:A.B(x) <= HTT";
 by (simp_tac (CCL_ss addsimps ([subsetXH,SgXH] @ HTT_rews)) 1);
 by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
-val SigmaF = result();
+qed "SigmaF";
 
 (*** Formation Rules for Recursive types - using coinduction these only need ***)
 (***                                          exhaution rule for type-former ***)
@@ -148,7 +148,7 @@
 by (etac HTT_coinduct3 1);
 by (fast_tac (set_cs addIs HTTgenIs 
                  addSEs [HTTgen_mono RS ci3_RI] addEs [XH_to_E NatXH]) 1);
-val NatF = result();
+qed "NatF";
 
 val [prem] = goal Hered.thy "A <= HTT ==> List(A) <= HTT";
 by (safe_tac set_cs);
@@ -156,7 +156,7 @@
 by (fast_tac (set_cs addSIs HTTgenIs 
                  addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] 
                  addEs [XH_to_E ListXH]) 1);
-val ListF = result();
+qed "ListF";
 
 val [prem] = goal Hered.thy "A <= HTT ==> Lists(A) <= HTT";
 by (safe_tac set_cs);
@@ -164,7 +164,7 @@
 by (fast_tac (set_cs addSIs HTTgenIs 
                  addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] 
                  addEs [XH_to_E ListsXH]) 1);
-val ListsF = result();
+qed "ListsF";
 
 val [prem] = goal Hered.thy "A <= HTT ==> ILists(A) <= HTT";
 by (safe_tac set_cs);
@@ -172,7 +172,7 @@
 by (fast_tac (set_cs addSIs HTTgenIs 
                  addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] 
                  addEs [XH_to_E IListsXH]) 1);
-val IListsF = result();
+qed "IListsF";
 
 (*** A possible use for this predicate is proving equality from pre-order       ***)
 (*** but it seems as easy (and more general) to do this directly by coinduction ***)
@@ -186,9 +186,9 @@
 by (REPEAT_SOME (rtac (POgenXH RS iffD2) ORELSE' etac rev_mp));
 by (ALLGOALS (simp_tac (term_ss addsimps HTT_rews)));
 by (ALLGOALS (fast_tac ccl_cs));
-val HTT_po_op = result();
+qed "HTT_po_op";
 
 val prems = goal Hered.thy "[| t : HTT;  t [= u |] ==> t = u";
 by (REPEAT (ares_tac (prems @ [conjI RS (eq_iff RS iffD2),HTT_po_op]) 1));
-val HTT_po_eq = result();
+qed "HTT_po_eq";
 *)
diff -r e0e5c1581e4c -r 2ca12511676d src/CCL/Lfp.ML
--- a/src/CCL/Lfp.ML	Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/Lfp.ML	Wed Nov 30 13:53:46 1994 +0100
@@ -18,27 +18,27 @@
 val prems = goalw Lfp.thy [lfp_def] "[| f(A) <= A |] ==> lfp(f) <= A";
 by (rtac (CollectI RS Inter_lower) 1);
 by (resolve_tac prems 1);
-val lfp_lowerbound = result();
+qed "lfp_lowerbound";
 
 val prems = goalw Lfp.thy [lfp_def]
     "[| !!u. f(u) <= u ==> A<=u |] ==> A <= lfp(f)";
 by (REPEAT (ares_tac ([Inter_greatest]@prems) 1));
 by (etac CollectD 1);
-val lfp_greatest = result();
+qed "lfp_greatest";
 
 val [mono] = goal Lfp.thy "mono(f) ==> f(lfp(f)) <= lfp(f)";
 by (EVERY1 [rtac lfp_greatest, rtac subset_trans,
 	    rtac (mono RS monoD), rtac lfp_lowerbound, atac, atac]);
-val lfp_lemma2 = result();
+qed "lfp_lemma2";
 
 val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) <= f(lfp(f))";
 by (EVERY1 [rtac lfp_lowerbound, rtac (mono RS monoD), 
 	    rtac lfp_lemma2, rtac mono]);
-val lfp_lemma3 = result();
+qed "lfp_lemma3";
 
 val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) = f(lfp(f))";
 by (REPEAT (resolve_tac [equalityI,lfp_lemma2,lfp_lemma3,mono] 1));
-val lfp_Tarski = result();
+qed "lfp_Tarski";
 
 
 (*** General induction rule for least fixed points ***)
@@ -53,14 +53,14 @@
 	    rtac (Int_lower1 RS (mono RS monoD)),
 	    rtac (mono RS lfp_lemma2),
 	    rtac (CollectI RS subsetI), rtac indhyp, atac]);
-val induct = result();
+qed "induct";
 
 (** Definition forms of lfp_Tarski and induct, to control unfolding **)
 
 val [rew,mono] = goal Lfp.thy "[| h==lfp(f);  mono(f) |] ==> h = f(h)";
 by (rewtac rew);
 by (rtac (mono RS lfp_Tarski) 1);
-val def_lfp_Tarski = result();
+qed "def_lfp_Tarski";
 
 val rew::prems = goal Lfp.thy
     "[| A == lfp(f);  a:A;  mono(f);   			\
@@ -68,7 +68,7 @@
 \    |] ==> P(a)";
 by (EVERY1 [rtac induct,	(*backtracking to force correct induction*)
 	    REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]);
-val def_induct = result();
+qed "def_induct";
 
 (*Monotonicity of lfp!*)
 val prems = goal Lfp.thy
@@ -78,5 +78,5 @@
 by (resolve_tac prems 1);
 by (rtac lfp_lemma2 1);
 by (resolve_tac prems 1);
-val lfp_mono = result();
+qed "lfp_mono";
 
diff -r e0e5c1581e4c -r 2ca12511676d src/CCL/Set.ML
--- a/src/CCL/Set.ML	Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/Set.ML	Wed Nov 30 13:53:46 1994 +0100
@@ -16,36 +16,36 @@
 val [prem] = goal Set.thy "[| P(a) |] ==> a : {x.P(x)}";
 by (rtac (mem_Collect_iff RS iffD2) 1);
 by (rtac prem 1);
-val CollectI = result();
+qed "CollectI";
 
 val prems = goal Set.thy "[| a : {x.P(x)} |] ==> P(a)";
 by (resolve_tac (prems RL [mem_Collect_iff  RS iffD1]) 1);
-val CollectD = result();
+qed "CollectD";
 
 val CollectE = make_elim CollectD;
 
 val [prem] = goal Set.thy "[| !!x. x:A <-> x:B |] ==> A = B";
 by (rtac (set_extension RS iffD2) 1);
 by (rtac (prem RS allI) 1);
-val set_ext = result();
+qed "set_ext";
 
 (*** Bounded quantifiers ***)
 
 val prems = goalw Set.thy [Ball_def]
     "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)";
 by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
-val ballI = result();
+qed "ballI";
 
 val [major,minor] = goalw Set.thy [Ball_def]
     "[| ALL x:A. P(x);  x:A |] ==> P(x)";
 by (rtac (minor RS (major RS spec RS mp)) 1);
-val bspec = result();
+qed "bspec";
 
 val major::prems = goalw Set.thy [Ball_def]
     "[| ALL x:A. P(x);  P(x) ==> Q;  ~ x:A ==> Q |] ==> Q";
 by (rtac (major RS spec RS impCE) 1);
 by (REPEAT (eresolve_tac prems 1));
-val ballE = result();
+qed "ballE";
 
 (*Takes assumptions ALL x:A.P(x) and a:A; creates assumption P(a)*)
 fun ball_tac i = etac ballE i THEN contr_tac (i+1);
@@ -53,9 +53,9 @@
 val prems = goalw Set.thy [Bex_def]
     "[| P(x);  x:A |] ==> EX x:A. P(x)";
 by (REPEAT (ares_tac (prems @ [exI,conjI]) 1));
-val bexI = result();
+qed "bexI";
 
-val bexCI = prove_goal Set.thy 
+qed_goal "bexCI" Set.thy 
    "[| EX x:A. ~P(x) ==> P(a);  a:A |] ==> EX x:A.P(x)"
  (fn prems=>
   [ (rtac classical 1),
@@ -65,13 +65,13 @@
     "[| EX x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q  |] ==> Q";
 by (rtac (major RS exE) 1);
 by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1));
-val bexE = result();
+qed "bexE";
 
 (*Trival rewrite rule;   (! x:A.P)=P holds only if A is nonempty!*)
 val prems = goal Set.thy
     "(ALL x:A. True) <-> True";
 by (REPEAT (ares_tac [TrueI,ballI,iffI] 1));
-val ball_rew = result();
+qed "ball_rew";
 
 (** Congruence rules **)
 
@@ -81,7 +81,7 @@
 by (resolve_tac (prems RL [ssubst,iffD2]) 1);
 by (REPEAT (ares_tac [ballI,iffI] 1
      ORELSE eresolve_tac ([make_elim bspec, mp] @ (prems RL [iffE])) 1));
-val ball_cong = result();
+qed "ball_cong";
 
 val prems = goal Set.thy
     "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==> \
@@ -89,37 +89,37 @@
 by (resolve_tac (prems RL [ssubst,iffD2]) 1);
 by (REPEAT (etac bexE 1
      ORELSE ares_tac ([bexI,iffI] @ (prems RL [iffD1,iffD2])) 1));
-val bex_cong = result();
+qed "bex_cong";
 
 (*** Rules for subsets ***)
 
 val prems = goalw Set.thy [subset_def] "(!!x.x:A ==> x:B) ==> A <= B";
 by (REPEAT (ares_tac (prems @ [ballI]) 1));
-val subsetI = result();
+qed "subsetI";
 
 (*Rule in Modus Ponens style*)
 val major::prems = goalw Set.thy [subset_def] "[| A <= B;  c:A |] ==> c:B";
 by (rtac (major RS bspec) 1);
 by (resolve_tac prems 1);
-val subsetD = result();
+qed "subsetD";
 
 (*Classical elimination rule*)
 val major::prems = goalw Set.thy [subset_def] 
     "[| A <= B;  ~(c:A) ==> P;  c:B ==> P |] ==> P";
 by (rtac (major RS ballE) 1);
 by (REPEAT (eresolve_tac prems 1));
-val subsetCE = result();
+qed "subsetCE";
 
 (*Takes assumptions A<=B; c:A and creates the assumption c:B *)
 fun set_mp_tac i = etac subsetCE i  THEN  mp_tac i;
 
-val subset_refl = prove_goal Set.thy "A <= A"
+qed_goal "subset_refl" Set.thy "A <= A"
  (fn _=> [ (REPEAT (ares_tac [subsetI] 1)) ]);
 
 goal Set.thy "!!A B C. [| A<=B;  B<=C |] ==> A<=C";
 by (rtac subsetI 1);
 by (REPEAT (eresolve_tac [asm_rl, subsetD] 1));
-val subset_trans = result();
+qed "subset_trans";
 
 
 (*** Rules for equality ***)
@@ -128,31 +128,31 @@
 val prems = goal Set.thy "[| A <= B;  B <= A |] ==> A = B";
 by (rtac (iffI RS set_ext) 1);
 by (REPEAT (ares_tac (prems RL [subsetD]) 1));
-val subset_antisym = result();
+qed "subset_antisym";
 val equalityI = subset_antisym;
 
 (* Equality rules from ZF set theory -- are they appropriate here? *)
 val prems = goal Set.thy "A = B ==> A<=B";
 by (resolve_tac (prems RL [subst]) 1);
 by (rtac subset_refl 1);
-val equalityD1 = result();
+qed "equalityD1";
 
 val prems = goal Set.thy "A = B ==> B<=A";
 by (resolve_tac (prems RL [subst]) 1);
 by (rtac subset_refl 1);
-val equalityD2 = result();
+qed "equalityD2";
 
 val prems = goal Set.thy
     "[| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P";
 by (resolve_tac prems 1);
 by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1));
-val equalityE = result();
+qed "equalityE";
 
 val major::prems = goal Set.thy
     "[| A = B;  [| c:A; c:B |] ==> P;  [| ~ c:A; ~ c:B |] ==> P |]  ==>  P";
 by (rtac (major RS equalityE) 1);
 by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1));
-val equalityCE = result();
+qed "equalityCE";
 
 (*Lemma for creating induction formulae -- for "pattern matching" on p
   To make the induction hypotheses usable, apply "spec" or "bspec" to
@@ -161,24 +161,24 @@
     "[| p:A;  !!z. z:A ==> p=z --> R |] ==> R";
 by (rtac mp 1);
 by (REPEAT (resolve_tac (refl::prems) 1));
-val setup_induction = result();
+qed "setup_induction";
 
 goal Set.thy "{x.x:A} = A";
 by (REPEAT (ares_tac [equalityI,subsetI,CollectI] 1  ORELSE etac CollectD 1));
-val trivial_set = result();
+qed "trivial_set";
 
 (*** Rules for binary union -- Un ***)
 
 val prems = goalw Set.thy [Un_def] "c:A ==> c : A Un B";
 by (REPEAT (resolve_tac (prems @ [CollectI,disjI1]) 1));
-val UnI1 = result();
+qed "UnI1";
 
 val prems = goalw Set.thy [Un_def] "c:B ==> c : A Un B";
 by (REPEAT (resolve_tac (prems @ [CollectI,disjI2]) 1));
-val UnI2 = result();
+qed "UnI2";
 
 (*Classical introduction rule: no commitment to A vs B*)
-val UnCI = prove_goal Set.thy "(~c:B ==> c:A) ==> c : A Un B"
+qed_goal "UnCI" Set.thy "(~c:B ==> c:A) ==> c : A Un B"
  (fn prems=>
   [ (rtac classical 1),
     (REPEAT (ares_tac (prems@[UnI1,notI]) 1)),
@@ -188,7 +188,7 @@
     "[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P";
 by (rtac (major RS CollectD RS disjE) 1);
 by (REPEAT (eresolve_tac prems 1));
-val UnE = result();
+qed "UnE";
 
 
 (*** Rules for small intersection -- Int ***)
@@ -196,22 +196,22 @@
 val prems = goalw Set.thy [Int_def]
     "[| c:A;  c:B |] ==> c : A Int B";
 by (REPEAT (resolve_tac (prems @ [CollectI,conjI]) 1));
-val IntI = result();
+qed "IntI";
 
 val [major] = goalw Set.thy [Int_def] "c : A Int B ==> c:A";
 by (rtac (major RS CollectD RS conjunct1) 1);
-val IntD1 = result();
+qed "IntD1";
 
 val [major] = goalw Set.thy [Int_def] "c : A Int B ==> c:B";
 by (rtac (major RS CollectD RS conjunct2) 1);
-val IntD2 = result();
+qed "IntD2";
 
 val [major,minor] = goal Set.thy
     "[| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P";
 by (rtac minor 1);
 by (rtac (major RS IntD1) 1);
 by (rtac (major RS IntD2) 1);
-val IntE = result();
+qed "IntE";
 
 
 (*** Rules for set complement -- Compl ***)
@@ -219,7 +219,7 @@
 val prems = goalw Set.thy [Compl_def]
     "[| c:A ==> False |] ==> c : Compl(A)";
 by (REPEAT (ares_tac (prems @ [CollectI,notI]) 1));
-val ComplI = result();
+qed "ComplI";
 
 (*This form, with negated conclusion, works well with the Classical prover.
   Negated assumptions behave like formulae on the right side of the notional
@@ -227,7 +227,7 @@
 val major::prems = goalw Set.thy [Compl_def]
     "[| c : Compl(A) |] ==> ~c:A";
 by (rtac (major RS CollectD) 1);
-val ComplD = result();
+qed "ComplD";
 
 val ComplE = make_elim ComplD;
 
@@ -236,11 +236,11 @@
 
 goalw Set.thy [empty_def] "{x.False} = {}";
 by (rtac refl 1);
-val empty_eq = result();
+qed "empty_eq";
 
 val [prem] = goalw Set.thy [empty_def] "a : {} ==> P";
 by (rtac (prem RS CollectD RS FalseE) 1);
-val emptyD = result();
+qed "emptyD";
 
 val emptyE = make_elim emptyD;
 
@@ -248,18 +248,18 @@
 by (rtac (prem RS swap) 1);
 by (rtac equalityI 1);
 by (ALLGOALS (fast_tac (FOL_cs addSIs [subsetI] addSEs [emptyD])));
-val not_emptyD = result();
+qed "not_emptyD";
 
 (*** Singleton sets ***)
 
 goalw Set.thy [singleton_def] "a : {a}";
 by (rtac CollectI 1);
 by (rtac refl 1);
-val singletonI = result();
+qed "singletonI";
 
 val [major] = goalw Set.thy [singleton_def] "b : {a} ==> b=a"; 
 by (rtac (major RS CollectD) 1);
-val singletonD = result();
+qed "singletonD";
 
 val singletonE = make_elim singletonD;
 
@@ -269,13 +269,13 @@
 val prems = goalw Set.thy [UNION_def]
     "[| a:A;  b: B(a) |] ==> b: (UN x:A. B(x))";
 by (REPEAT (resolve_tac (prems @ [bexI,CollectI]) 1));
-val UN_I = result();
+qed "UN_I";
 
 val major::prems = goalw Set.thy [UNION_def]
     "[| b : (UN x:A. B(x));  !!x.[| x:A;  b: B(x) |] ==> R |] ==> R";
 by (rtac (major RS CollectD RS bexE) 1);
 by (REPEAT (ares_tac prems 1));
-val UN_E = result();
+qed "UN_E";
 
 val prems = goal Set.thy
     "[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==> \
@@ -283,27 +283,27 @@
 by (REPEAT (etac UN_E 1
      ORELSE ares_tac ([UN_I,equalityI,subsetI] @ 
 		      (prems RL [equalityD1,equalityD2] RL [subsetD])) 1));
-val UN_cong = result();
+qed "UN_cong";
 
 (*** Intersections of families -- INTER x:A. B(x) is Inter(B)``A ) *)
 
 val prems = goalw Set.thy [INTER_def]
     "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))";
 by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1));
-val INT_I = result();
+qed "INT_I";
 
 val major::prems = goalw Set.thy [INTER_def]
     "[| b : (INT x:A. B(x));  a:A |] ==> b: B(a)";
 by (rtac (major RS CollectD RS bspec) 1);
 by (resolve_tac prems 1);
-val INT_D = result();
+qed "INT_D";
 
 (*"Classical" elimination rule -- does not require proving X:C *)
 val major::prems = goalw Set.thy [INTER_def]
     "[| b : (INT x:A. B(x));  b: B(a) ==> R;  ~ a:A ==> R |] ==> R";
 by (rtac (major RS CollectD RS ballE) 1);
 by (REPEAT (eresolve_tac prems 1));
-val INT_E = result();
+qed "INT_E";
 
 val prems = goal Set.thy
     "[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==> \
@@ -311,7 +311,7 @@
 by (REPEAT_FIRST (resolve_tac [INT_I,equalityI,subsetI]));
 by (REPEAT (dtac INT_D 1
      ORELSE ares_tac (prems RL [equalityD1,equalityD2] RL [subsetD]) 1));
-val INT_cong = result();
+qed "INT_cong";
 
 (*** Rules for Unions ***)
 
@@ -319,20 +319,20 @@
 val prems = goalw Set.thy [Union_def]
     "[| X:C;  A:X |] ==> A : Union(C)";
 by (REPEAT (resolve_tac (prems @ [UN_I]) 1));
-val UnionI = result();
+qed "UnionI";
 
 val major::prems = goalw Set.thy [Union_def]
     "[| A : Union(C);  !!X.[| A:X;  X:C |] ==> R |] ==> R";
 by (rtac (major RS UN_E) 1);
 by (REPEAT (ares_tac prems 1));
-val UnionE = result();
+qed "UnionE";
 
 (*** Rules for Inter ***)
 
 val prems = goalw Set.thy [Inter_def]
     "[| !!X. X:C ==> A:X |] ==> A : Inter(C)";
 by (REPEAT (ares_tac ([INT_I] @ prems) 1));
-val InterI = result();
+qed "InterI";
 
 (*A "destruct" rule -- every X in C contains A as an element, but
   A:X can hold when X:C does not!  This rule is analogous to "spec". *)
@@ -340,11 +340,11 @@
     "[| A : Inter(C);  X:C |] ==> A:X";
 by (rtac (major RS INT_D) 1);
 by (resolve_tac prems 1);
-val InterD = result();
+qed "InterD";
 
 (*"Classical" elimination rule -- does not require proving X:C *)
 val major::prems = goalw Set.thy [Inter_def]
     "[| A : Inter(C);  A:X ==> R;  ~ X:C ==> R |] ==> R";
 by (rtac (major RS INT_E) 1);
 by (REPEAT (eresolve_tac prems 1));
-val InterE = result();
+qed "InterE";
diff -r e0e5c1581e4c -r 2ca12511676d src/CCL/Term.ML
--- a/src/CCL/Term.ML	Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/Term.ML	Wed Nov 30 13:53:46 1994 +0100
@@ -24,34 +24,34 @@
 goalw Term.thy [let_def] "~ t=bot--> let x be t in f(x) = f(t)";
 by (res_inst_tac [("t","t")] term_case 1);
 by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
-val letB = result() RS mp;
+val letB = store_thm("letB", result() RS mp);
 
 goalw Term.thy [let_def] "let x be bot in f(x) = bot";
 by (rtac caseBbot 1);
-val letBabot = result();
+qed "letBabot";
 
 goalw Term.thy [let_def] "let x be t in bot = bot";
 by (resolve_tac ([caseBbot] RL [term_case]) 1);
 by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
-val letBbbot = result();
+qed "letBbbot";
 
 goalw Term.thy [apply_def] "(lam x.b(x)) ` a = b(a)";
 by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
-val applyB = result();
+qed "applyB";
 
 goalw Term.thy [apply_def] "bot ` a = bot";
 by (rtac caseBbot 1);
-val applyBbot = result();
+qed "applyBbot";
 
 goalw Term.thy [fix_def] "fix(f) = f(fix(f))";
 by (resolve_tac [applyB RS ssubst] 1 THEN rtac refl 1);
-val fixB = result();
+qed "fixB";
 
 goalw Term.thy [letrec_def]
       "letrec g x be h(x,g) in g(a) = h(a,%y.letrec g x be h(x,g) in g(y))";
 by (resolve_tac [fixB RS ssubst] 1 THEN 
     resolve_tac [applyB RS ssubst] 1 THEN rtac refl 1);
-val letrecB = result();
+qed "letrecB";
 
 val rawBs = caseBs @ [applyB,applyBbot];
 
diff -r e0e5c1581e4c -r 2ca12511676d src/CCL/Trancl.ML
--- a/src/CCL/Trancl.ML	Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/Trancl.ML	Wed Nov 30 13:53:46 1994 +0100
@@ -17,13 +17,13 @@
 val prems = goalw Trancl.thy [trans_def]
     "(!! x y z. [| <x,y>:r;  <y,z>:r |] ==> <x,z>:r) ==> trans(r)";
 by (REPEAT (ares_tac (prems@[allI,impI]) 1));
-val transI = result();
+qed "transI";
 
 val major::prems = goalw Trancl.thy [trans_def]
     "[| trans(r);  <a,b>:r;  <b,c>:r |] ==> <a,c>:r";
 by (cut_facts_tac [major] 1);
 by (fast_tac (FOL_cs addIs prems) 1);
-val transD = result();
+qed "transD";
 
 (** Identity relation **)
 
@@ -31,7 +31,7 @@
 by (rtac CollectI 1);
 by (rtac exI 1);
 by (rtac refl 1);
-val idI = result();
+qed "idI";
 
 val major::prems = goalw Trancl.thy [id_def]
     "[| p: id;  !!x.[| p = <x,x> |] ==> P  \
@@ -39,14 +39,14 @@
 by (rtac (major RS CollectE) 1);
 by (etac exE 1);
 by (eresolve_tac prems 1);
-val idE = result();
+qed "idE";
 
 (** Composition of two relations **)
 
 val prems = goalw Trancl.thy [comp_def]
     "[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s";
 by (fast_tac (set_cs addIs prems) 1);
-val compI = result();
+qed "compI";
 
 (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
 val prems = goalw Trancl.thy [comp_def]
@@ -55,7 +55,7 @@
 \    |] ==> P";
 by (cut_facts_tac prems 1);
 by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1));
-val compE = result();
+qed "compE";
 
 val prems = goal Trancl.thy
     "[| <a,c> : r O s;  \
@@ -63,7 +63,7 @@
 \    |] ==> P";
 by (rtac compE 1);
 by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [pair_inject,ssubst] 1));
-val compEpair = result();
+qed "compEpair";
 
 val comp_cs = set_cs addIs [compI,idI] 
 		       addEs [compE,idE] 
@@ -73,14 +73,14 @@
     "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
 by (cut_facts_tac prems 1);
 by (fast_tac comp_cs 1);
-val comp_mono = result();
+qed "comp_mono";
 
 (** The relation rtrancl **)
 
 goal Trancl.thy "mono(%s. id Un (r O s))";
 by (rtac monoI 1);
 by (REPEAT (ares_tac [monoI, subset_refl, comp_mono, Un_mono] 1));
-val rtrancl_fun_mono = result();
+qed "rtrancl_fun_mono";
 
 val rtrancl_unfold = rtrancl_fun_mono RS (rtrancl_def RS def_lfp_Tarski);
 
@@ -88,20 +88,20 @@
 goal Trancl.thy "<a,a> : r^*";
 by (rtac (rtrancl_unfold RS ssubst) 1);
 by (fast_tac comp_cs 1);
-val rtrancl_refl = result();
+qed "rtrancl_refl";
 
 (*Closure under composition with r*)
 val prems = goal Trancl.thy
     "[| <a,b> : r^*;  <b,c> : r |] ==> <a,c> : r^*";
 by (rtac (rtrancl_unfold RS ssubst) 1);
 by (fast_tac (comp_cs addIs prems) 1);
-val rtrancl_into_rtrancl = result();
+qed "rtrancl_into_rtrancl";
 
 (*rtrancl of r contains r*)
 val [prem] = goal Trancl.thy "[| <a,b> : r |] ==> <a,b> : r^*";
 by (rtac (rtrancl_refl RS rtrancl_into_rtrancl) 1);
 by (rtac prem 1);
-val r_into_rtrancl = result();
+qed "r_into_rtrancl";
 
 
 (** standard induction rule **)
@@ -114,7 +114,7 @@
 by (rtac (major RS (rtrancl_def RS def_induct)) 1);
 by (rtac rtrancl_fun_mono 1);
 by (fast_tac (comp_cs addIs prems) 1);
-val rtrancl_full_induct = result();
+qed "rtrancl_full_induct";
 
 (*nice induction rule*)
 val major::prems = goal Trancl.thy
@@ -130,14 +130,14 @@
 by (resolve_tac [major RS rtrancl_full_induct] 1);
 by (fast_tac (comp_cs addIs prems) 1);
 by (fast_tac (comp_cs addIs prems) 1);
-val rtrancl_induct = result();
+qed "rtrancl_induct";
 
 (*transitivity of transitive closure!! -- by induction.*)
 goal Trancl.thy "trans(r^*)";
 by (rtac transI 1);
 by (res_inst_tac [("b","z")] rtrancl_induct 1);
 by (DEPTH_SOLVE (eresolve_tac [asm_rl, rtrancl_into_rtrancl] 1));
-val trans_rtrancl = result();
+qed "trans_rtrancl";
 
 (*elimination of rtrancl -- by induction on a special formula*)
 val major::prems = goal Trancl.thy
@@ -149,7 +149,7 @@
 by (fast_tac (set_cs addIs prems) 2);
 by (fast_tac (set_cs addIs prems) 2);
 by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
-val rtranclE = result();
+qed "rtranclE";
 
 
 (**** The relation trancl ****)
@@ -160,19 +160,19 @@
     "[| <a,b> : r^+ |] ==> <a,b> : r^*";
 by (resolve_tac [major RS compEpair] 1);
 by (REPEAT (ares_tac [rtrancl_into_rtrancl] 1));
-val trancl_into_rtrancl = result();
+qed "trancl_into_rtrancl";
 
 (*r^+ contains r*)
 val [prem] = goalw Trancl.thy [trancl_def]
    "[| <a,b> : r |] ==> <a,b> : r^+";
 by (REPEAT (ares_tac [prem,compI,rtrancl_refl] 1));
-val r_into_trancl = result();
+qed "r_into_trancl";
 
 (*intro rule by definition: from rtrancl and r*)
 val prems = goalw Trancl.thy [trancl_def]
     "[| <a,b> : r^*;  <b,c> : r |]   ==>  <a,c> : r^+";
 by (REPEAT (resolve_tac ([compI]@prems) 1));
-val rtrancl_into_trancl1 = result();
+qed "rtrancl_into_trancl1";
 
 (*intro rule from r and rtrancl*)
 val prems = goal Trancl.thy
@@ -182,7 +182,7 @@
 by (resolve_tac (prems RL [r_into_trancl]) 1);
 by (rtac (trans_rtrancl RS transD RS rtrancl_into_trancl1) 1);
 by (REPEAT (ares_tac (prems@[r_into_rtrancl]) 1));
-val rtrancl_into_trancl2 = result();
+qed "rtrancl_into_trancl2";
 
 (*elimination of r^+ -- NOT an induction rule*)
 val major::prems = goal Trancl.thy
@@ -196,7 +196,7 @@
 by (etac rtranclE 1);
 by (fast_tac comp_cs 1);
 by (fast_tac (comp_cs addSIs [rtrancl_into_trancl1]) 1);
-val tranclE = result();
+qed "tranclE";
 
 (*Transitivity of r^+.
   Proved by unfolding since it uses transitivity of rtrancl. *)
@@ -205,11 +205,11 @@
 by (REPEAT (etac compEpair 1));
 by (rtac (rtrancl_into_rtrancl RS (trans_rtrancl RS transD RS compI)) 1);
 by (REPEAT (assume_tac 1));
-val trans_trancl = result();
+qed "trans_trancl";
 
 val prems = goal Trancl.thy
     "[| <a,b> : r;  <b,c> : r^+ |]   ==>  <a,c> : r^+";
 by (rtac (r_into_trancl RS (trans_trancl RS transD)) 1);
 by (resolve_tac prems 1);
 by (resolve_tac prems 1);
-val trancl_into_trancl2 = result();
+qed "trancl_into_trancl2";
diff -r e0e5c1581e4c -r 2ca12511676d src/CCL/Type.ML
--- a/src/CCL/Type.ML	Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/Type.ML	Wed Nov 30 13:53:46 1994 +0100
@@ -17,7 +17,7 @@
 
 goal Set.thy "A <= B <-> (ALL x.x:A --> x:B)";
 by (fast_tac set_cs 1);
-val subsetXH = result();
+qed "subsetXH";
 
 (*** Exhaustion Rules ***)
 
@@ -99,22 +99,22 @@
 val prems = goal Type.thy
      "[| a:A;  P(a) |] ==> a : {x:A. P(x)}";
 by (REPEAT (resolve_tac (prems@[SubtypeXH RS iffD2,conjI]) 1));
-val SubtypeI = result();
+qed "SubtypeI";
 
 val prems = goal Type.thy
      "[| a : {x:A. P(x)};  [| a:A;  P(a) |] ==> Q |] ==> Q";
 by (REPEAT (resolve_tac (prems@[SubtypeD1,SubtypeD2]) 1));
-val SubtypeE = result();
+qed "SubtypeE";
 
 (*** Monotonicity ***)
 
 goal Type.thy "mono (%X.X)";
 by (REPEAT (ares_tac [monoI] 1));
-val idM = result();
+qed "idM";
 
 goal Type.thy "mono(%X.A)";
 by (REPEAT (ares_tac [monoI,subset_refl] 1));
-val constM = result();
+qed "constM";
 
 val major::prems = goal Type.thy
     "mono(%X.A(X)) ==> mono(%X.[A(X)])";
@@ -125,7 +125,7 @@
 by (rtac (disjI2 RS (LiftXH RS iffD2)) 1);
 by (etac (major RS monoD RS subsetD) 1);
 by (assume_tac 1);
-val LiftM = result();
+qed "LiftM";
 
 val prems = goal Type.thy
     "[| mono(%X.A(X)); !!x X. x:A(X) ==> mono(%X.B(X,x)) |] ==> \
@@ -134,7 +134,7 @@
             eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
             (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
             hyp_subst_tac 1));
-val SgM = result();
+qed "SgM";
 
 val prems = goal Type.thy
     "[| !!x. x:A ==> mono(%X.B(X,x)) |] ==> mono(%X.Pi(A,B(X)))";
@@ -142,7 +142,7 @@
             eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
             (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
             hyp_subst_tac 1));
-val PiM = result();
+qed "PiM";
 
 val prems = goal Type.thy
      "[| mono(%X.A(X));  mono(%X.B(X)) |] ==> mono(%X.A(X)+B(X))";
@@ -150,7 +150,7 @@
             eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
             (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
             hyp_subst_tac 1));
-val PlusM = result();
+qed "PlusM";
 
 (**************** RECURSIVE TYPES ******************)
 
@@ -158,19 +158,19 @@
 
 goal Type.thy "mono(%X.Unit+X)";
 by (REPEAT (ares_tac [PlusM,constM,idM] 1));
-val NatM = result();
-val def_NatB = result() RS (Nat_def RS def_lfp_Tarski);
+qed "NatM";
+val def_NatB = store_thm("def_NatB", result() RS (Nat_def RS def_lfp_Tarski));
 
 goal Type.thy "mono(%X.(Unit+Sigma(A,%y.X)))";
 by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
-val ListM = result();
-val def_ListB = result() RS (List_def RS def_lfp_Tarski);
-val def_ListsB = result() RS (Lists_def RS def_gfp_Tarski);
+qed "ListM";
+val def_ListB = store_thm("def_ListB", result() RS (List_def RS def_lfp_Tarski));
+val def_ListsB = store_thm("def_ListsB", result() RS (Lists_def RS def_gfp_Tarski));
 
 goal Type.thy "mono(%X.({} + Sigma(A,%y.X)))";
 by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
-val IListsM = result();
-val def_IListsB = result() RS (ILists_def RS def_gfp_Tarski);
+qed "IListsM";
+val def_IListsB = store_thm("def_IListsB", result() RS (ILists_def RS def_gfp_Tarski));
 
 val ind_type_eqs = [def_NatB,def_ListB,def_ListsB,def_IListsB];
 
@@ -264,7 +264,7 @@
 by (rtac (major RS (XH_to_E SgXH)) 1);
 by (rtac minor 1);
 by (ALLGOALS (fast_tac term_cs));
-val SgE2 = result();
+qed "SgE2";
 
 (* General theorem proving ignores non-canonical term-formers,             *)
 (*         - intro rules are type rules for canonical terms                *)
@@ -280,7 +280,7 @@
 by (rtac (lfp_lowerbound RS subset_trans) 1);
 by (rtac (mono RS gfp_lemma3) 1);
 by (rtac subset_refl 1);
-val lfp_subset_gfp = result();
+qed "lfp_subset_gfp";
 
 val prems = goal Type.thy
     "[| a:A;  !!x X.[| x:A;  ALL y:A.t(y):X |] ==> t(x) : B(X) |] ==> \
@@ -288,14 +288,14 @@
 by (rtac coinduct 1);
 by (res_inst_tac [("P","%x.EX y:A.x=t(y)")] CollectI 1);
 by (ALLGOALS (fast_tac (ccl_cs addSIs prems)));
-val gfpI = result();
+qed "gfpI";
 
 val rew::prem::prems = goal Type.thy
     "[| C==gfp(B);  a:A;  !!x X.[| x:A;  ALL y:A.t(y):X |] ==> t(x) : B(X) |] ==> \
 \    t(a) : C";
 by (rewtac rew);
 by (REPEAT (ares_tac ((prem RS gfpI)::prems) 1));
-val def_gfpI = result();
+qed "def_gfpI";
 
 (* EG *)
 
diff -r e0e5c1581e4c -r 2ca12511676d src/CCL/Wfd.ML
--- a/src/CCL/Wfd.ML	Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/Wfd.ML	Wed Nov 30 13:53:46 1994 +0100
@@ -20,7 +20,7 @@
 \    P(a)";
 by (rtac (major RS spec RS mp RS spec RS CollectD) 1);
 by (fast_tac (set_cs addSIs [prem RS CollectI]) 1);
-val wfd_induct = result();
+qed "wfd_induct";
 
 val [p1,p2,p3] = goal Wfd.thy
     "[| !!x y.<x,y> : R ==> Q(x); \
@@ -28,7 +28,7 @@
 \       !!x.Q(x) ==> x:P |] ==> a:P";
 by (rtac (p2 RS  spec  RS mp) 1);
 by (fast_tac (set_cs addSIs [p1 RS p3]) 1);
-val wfd_strengthen_lemma = result();
+qed "wfd_strengthen_lemma";
 
 fun wfd_strengthen_tac s i = res_inst_tac [("Q",s)] wfd_strengthen_lemma i THEN
                              assume_tac (i+1);
@@ -38,12 +38,12 @@
 by (fast_tac (FOL_cs addIs prems) 1);
 by (rtac (wfd RS  wfd_induct) 1);
 by (ALLGOALS (fast_tac (ccl_cs addSIs prems)));
-val wf_anti_sym = result();
+qed "wf_anti_sym";
 
 val prems = goal Wfd.thy "[| Wfd(r);  <a,a>: r |] ==> P";
 by (rtac wf_anti_sym 1);
 by (REPEAT (resolve_tac prems 1));
-val wf_anti_refl = result();
+qed "wf_anti_refl";
 
 (*** Irreflexive transitive closure ***)
 
@@ -59,24 +59,24 @@
 by (fast_tac ccl_cs 1);
 by (etac (spec RS mp RS spec RS mp) 1);
 by (REPEAT (atac 1));
-val trancl_wf = result();
+qed "trancl_wf";
 
 (*** Lexicographic Ordering ***)
 
 goalw Wfd.thy [lex_def] 
  "p : ra**rb <-> (EX a a' b b'.p = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb))";
 by (fast_tac ccl_cs 1);
-val lexXH = result();
+qed "lexXH";
 
 val prems = goal Wfd.thy
  "<a,a'> : ra ==> <<a,b>,<a',b'>> : ra**rb";
 by (fast_tac (ccl_cs addSIs (prems @ [lexXH RS iffD2])) 1);
-val lexI1 = result();
+qed "lexI1";
 
 val prems = goal Wfd.thy
  "<b,b'> : rb ==> <<a,b>,<a,b'>> : ra**rb";
 by (fast_tac (ccl_cs addSIs (prems @ [lexXH RS iffD2])) 1);
-val lexI2 = result();
+qed "lexI2";
 
 val major::prems = goal Wfd.thy
  "[| p : ra**rb;  \
@@ -86,13 +86,13 @@
 by (rtac (major RS (lexXH RS iffD1) RS exE) 1);
 by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems)));
 by (ALLGOALS (fast_tac ccl_cs));
-val lexE = result();
+qed "lexE";
 
 val [major,minor] = goal Wfd.thy
  "[| p : r**s;  !!a a' b b'. p = <<a,b>,<a',b'>> ==> P |] ==>P";
 by (rtac (major RS lexE) 1);
 by (ALLGOALS (fast_tac (set_cs addSEs [minor])));
-val lex_pair = result();
+qed "lex_pair";
 
 val [wfa,wfb] = goal Wfd.thy
  "[| Wfd(R); Wfd(S) |] ==> Wfd(R**S)";
@@ -105,26 +105,26 @@
 by (rtac (wfa RS wfd_induct RS allI) 1);
 by (rtac (wfb RS wfd_induct RS allI) 1);back();
 by (fast_tac (type_cs addSEs [lexE]) 1);
-val lex_wf = result();
+qed "lex_wf";
 
 (*** Mapping ***)
 
 goalw Wfd.thy [wmap_def] 
  "p : wmap(f,r) <-> (EX x y. p=<x,y>  &  <f(x),f(y)> : r)";
 by (fast_tac ccl_cs 1);
-val wmapXH = result();
+qed "wmapXH";
 
 val prems = goal Wfd.thy
  "<f(a),f(b)> : r ==> <a,b> : wmap(f,r)";
 by (fast_tac (ccl_cs addSIs (prems @ [wmapXH RS iffD2])) 1);
-val wmapI = result();
+qed "wmapI";
 
 val major::prems = goal Wfd.thy
  "[| p : wmap(f,r);  !!a b.[| <f(a),f(b)> : r;  p=<a,b> |] ==> R |] ==> R";
 by (rtac (major RS (wmapXH RS iffD1) RS exE) 1);
 by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems)));
 by (ALLGOALS (fast_tac ccl_cs));
-val wmapE = result();
+qed "wmapE";
 
 val [wf] = goal Wfd.thy
  "Wfd(r) ==> Wfd(wmap(f,r))";
@@ -139,49 +139,49 @@
 by (etac (spec RS mp RS spec RS mp) 1);
 by (assume_tac 1);
 by (rtac refl 1);
-val wmap_wf = result();
+qed "wmap_wf";
 
 (* Projections *)
 
 val prems = goal Wfd.thy "<xa,ya> : r ==> <<xa,xb>,<ya,yb>> : wmap(fst,r)";
 by (rtac wmapI 1);
 by (simp_tac (term_ss addsimps prems) 1);
-val wfstI = result();
+qed "wfstI";
 
 val prems = goal Wfd.thy "<xb,yb> : r ==> <<xa,xb>,<ya,yb>> : wmap(snd,r)";
 by (rtac wmapI 1);
 by (simp_tac (term_ss addsimps prems) 1);
-val wsndI = result();
+qed "wsndI";
 
 val prems = goal Wfd.thy "<xc,yc> : r ==> <<xa,<xb,xc>>,<ya,<yb,yc>>> : wmap(thd,r)";
 by (rtac wmapI 1);
 by (simp_tac (term_ss addsimps prems) 1);
-val wthdI = result();
+qed "wthdI";
 
 (*** Ground well-founded relations ***)
 
 val prems = goalw Wfd.thy [wf_def] 
     "[| Wfd(r);  a : r |] ==> a : wf(r)";
 by (fast_tac (set_cs addSIs prems) 1);
-val wfI = result();
+qed "wfI";
 
 val prems = goalw Wfd.thy [Wfd_def] "Wfd({})";
 by (fast_tac (set_cs addEs [EmptyXH RS iffD1 RS FalseE]) 1);
-val Empty_wf = result();
+qed "Empty_wf";
 
 val prems = goalw Wfd.thy [wf_def] "Wfd(wf(R))";
 by (res_inst_tac [("Q","Wfd(R)")] (excluded_middle RS disjE) 1);
 by (ALLGOALS (asm_simp_tac CCL_ss));
 by (rtac Empty_wf 1);
-val wf_wf = result();
+qed "wf_wf";
 
 goalw Wfd.thy [NatPR_def]  "p : NatPR <-> (EX x:Nat.p=<x,succ(x)>)";
 by (fast_tac set_cs 1);
-val NatPRXH = result();
+qed "NatPRXH";
 
 goalw Wfd.thy [ListPR_def]  "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h$t>)";
 by (fast_tac set_cs 1);
-val ListPRXH = result();
+qed "ListPRXH";
 
 val NatPRI = refl RS (bexI RS (NatPRXH RS iffD2));
 val ListPRI = refl RS (bexI RS (bexI RS (ListPRXH RS iffD2)));
@@ -192,7 +192,7 @@
 by (fast_tac (type_cs addSEs [XH_to_E NatPRXH]) 1);
 by (etac Nat_ind 1);
 by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E NatPRXH])));
-val NatPR_wf = result();
+qed "NatPR_wf";
 
 goalw Wfd.thy [Wfd_def]  "Wfd(ListPR(A))";
 by (safe_tac set_cs);
@@ -200,5 +200,5 @@
 by (fast_tac (type_cs addSEs [XH_to_E ListPRXH]) 1);
 by (etac List_ind 1);
 by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E ListPRXH])));
-val ListPR_wf = result();
+qed "ListPR_wf";
 
diff -r e0e5c1581e4c -r 2ca12511676d src/CCL/coinduction.ML
--- a/src/CCL/coinduction.ML	Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/coinduction.ML	Wed Nov 30 13:53:46 1994 +0100
@@ -9,15 +9,15 @@
 val [mono,prem] = goal Lfp.thy "[| mono(f);  a : f(lfp(f)) |] ==> a : lfp(f)";
 by (rtac ((mono RS lfp_Tarski) RS ssubst) 1);
 by (rtac prem 1);
-val lfpI = result();
+qed "lfpI";
 
 val prems = goal CCL.thy "[| a=a';  a' : A |] ==> a : A";
 by (simp_tac (term_ss addsimps prems) 1);
-val ssubst_single = result();
+qed "ssubst_single";
 
 val prems = goal CCL.thy "[| a=a';  b=b';  <a',b'> : A |] ==> <a,b> : A";
 by (simp_tac (term_ss addsimps prems) 1);
-val ssubst_pair = result();
+qed "ssubst_pair";
 
 (***)
 
@@ -42,7 +42,7 @@
 
 goal Term.thy "<a,a> : PO";
 by (rtac (po_refl RS (XH_to_D PO_iff)) 1);
-val PO_refl = result();
+qed "PO_refl";
 
 val POgenIs = map (mk_genIs Term.thy data_defs POgenXH POgen_mono)
       ["<true,true> : POgen(R)",
@@ -72,7 +72,7 @@
 
 goal Term.thy "<a,a> : EQ";
 by (rtac (refl RS (EQ_iff RS iffD1)) 1);
-val EQ_refl = result();
+qed "EQ_refl";
 
 val EQgenIs = map (mk_genIs Term.thy data_defs EQgenXH EQgen_mono)
 ["<true,true> : EQgen(R)",
diff -r e0e5c1581e4c -r 2ca12511676d src/CCL/equalities.ML
--- a/src/CCL/equalities.ML	Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/equalities.ML	Wed Nov 30 13:53:46 1994 +0100
@@ -17,118 +17,118 @@
 
 goal Set.thy "A Int A = A";
 by (fast_tac eq_cs 1);
-val Int_absorb = result();
+qed "Int_absorb";
 
 goal Set.thy "A Int B  =  B Int A";
 by (fast_tac eq_cs 1);
-val Int_commute = result();
+qed "Int_commute";
 
 goal Set.thy "(A Int B) Int C  =  A Int (B Int C)";
 by (fast_tac eq_cs 1);
-val Int_assoc = result();
+qed "Int_assoc";
 
 goal Set.thy "(A Un B) Int C  =  (A Int C) Un (B Int C)";
 by (fast_tac eq_cs 1);
-val Int_Un_distrib = result();
+qed "Int_Un_distrib";
 
 goal Set.thy "(A<=B) <-> (A Int B = A)";
 by (fast_tac (eq_cs addSEs [equalityE]) 1);
-val subset_Int_eq = result();
+qed "subset_Int_eq";
 
 (** Binary Union **)
 
 goal Set.thy "A Un A = A";
 by (fast_tac eq_cs 1);
-val Un_absorb = result();
+qed "Un_absorb";
 
 goal Set.thy "A Un B  =  B Un A";
 by (fast_tac eq_cs 1);
-val Un_commute = result();
+qed "Un_commute";
 
 goal Set.thy "(A Un B) Un C  =  A Un (B Un C)";
 by (fast_tac eq_cs 1);
-val Un_assoc = result();
+qed "Un_assoc";
 
 goal Set.thy "(A Int B) Un C  =  (A Un C) Int (B Un C)";
 by (fast_tac eq_cs 1);
-val Un_Int_distrib = result();
+qed "Un_Int_distrib";
 
 goal Set.thy
  "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
 by (fast_tac eq_cs 1);
-val Un_Int_crazy = result();
+qed "Un_Int_crazy";
 
 goal Set.thy "(A<=B) <-> (A Un B = B)";
 by (fast_tac (eq_cs addSEs [equalityE]) 1);
-val subset_Un_eq = result();
+qed "subset_Un_eq";
 
 (** Simple properties of Compl -- complement of a set **)
 
 goal Set.thy "A Int Compl(A) = {x.False}";
 by (fast_tac eq_cs 1);
-val Compl_disjoint = result();
+qed "Compl_disjoint";
 
 goal Set.thy "A Un Compl(A) = {x.True}";
 by (fast_tac eq_cs 1);
-val Compl_partition = result();
+qed "Compl_partition";
 
 goal Set.thy "Compl(Compl(A)) = A";
 by (fast_tac eq_cs 1);
-val double_complement = result();
+qed "double_complement";
 
 goal Set.thy "Compl(A Un B) = Compl(A) Int Compl(B)";
 by (fast_tac eq_cs 1);
-val Compl_Un = result();
+qed "Compl_Un";
 
 goal Set.thy "Compl(A Int B) = Compl(A) Un Compl(B)";
 by (fast_tac eq_cs 1);
-val Compl_Int = result();
+qed "Compl_Int";
 
 goal Set.thy "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))";
 by (fast_tac eq_cs 1);
-val Compl_UN = result();
+qed "Compl_UN";
 
 goal Set.thy "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))";
 by (fast_tac eq_cs 1);
-val Compl_INT = result();
+qed "Compl_INT";
 
 (*Halmos, Naive Set Theory, page 16.*)
 
 goal Set.thy "((A Int B) Un C = A Int (B Un C)) <-> (C<=A)";
 by (fast_tac (eq_cs addSEs [equalityE]) 1);
-val Un_Int_assoc_eq = result();
+qed "Un_Int_assoc_eq";
 
 
 (** Big Union and Intersection **)
 
 goal Set.thy "Union(A Un B) = Union(A) Un Union(B)";
 by (fast_tac eq_cs 1);
-val Union_Un_distrib = result();
+qed "Union_Un_distrib";
 
 val prems = goal Set.thy
    "(Union(C) Int A = {x.False}) <-> (ALL B:C. B Int A = {x.False})";
 by (fast_tac (eq_cs addSEs [equalityE]) 1);
-val Union_disjoint = result();
+qed "Union_disjoint";
 
 goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)";
 by (best_tac eq_cs 1);
-val Inter_Un_distrib = result();
+qed "Inter_Un_distrib";
 
 (** Unions and Intersections of Families **)
 
 goal Set.thy "(UN x:A. B(x)) = Union({Y. EX x:A. Y=B(x)})";
 by (fast_tac eq_cs 1);
-val UN_eq = result();
+qed "UN_eq";
 
 (*Look: it has an EXISTENTIAL quantifier*)
 goal Set.thy "(INT x:A. B(x)) = Inter({Y. EX x:A. Y=B(x)})";
 by (fast_tac eq_cs 1);
-val INT_eq = result();
+qed "INT_eq";
 
 goal Set.thy "A Int Union(B) = (UN C:B. A Int C)";
 by (fast_tac eq_cs 1);
-val Int_Union_image = result();
+qed "Int_Union_image";
 
 goal Set.thy "A Un Inter(B) = (INT C:B. A Un C)";
 by (fast_tac eq_cs 1);
-val Un_Inter_image = result();
+qed "Un_Inter_image";
diff -r e0e5c1581e4c -r 2ca12511676d src/CCL/eval.ML
--- a/src/CCL/eval.ML	Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/eval.ML	Wed Nov 30 13:53:46 1994 +0100
@@ -16,7 +16,7 @@
 val prems = goalw thy [apply_def]
    "[| f ---> lam x.b(x);  b(a) ---> c |] ==> f ` a ---> c";
 by (ceval_tac prems);
-val applyV = result();
+qed "applyV";
 
 EVal_rls := !EVal_rls @ [applyV];
 
@@ -25,20 +25,20 @@
 by (rtac (major RS canonical) 1);
 by (REPEAT (DEPTH_SOLVE_1 (resolve_tac ([major]@prems@(!EVal_rls)) 1 ORELSE
                            etac substitute 1)));
-val letV = result();
+qed "letV";
 
 val prems = goalw thy [fix_def]
    "f(fix(f)) ---> c ==> fix(f) ---> c";
 by (rtac applyV 1);
 by (rtac lamV 1);
 by (resolve_tac prems 1);
-val fixV = result();
+qed "fixV";
 
 val prems = goalw thy [letrec_def]
     "h(t,%y.letrec g x be h(x,g) in g(y)) ---> c ==> \
 \                  letrec g x be h(x,g) in g(t) ---> c";
 by (REPEAT (resolve_tac (prems @ [fixV,applyV,lamV]) 1));
-val letrecV = result();
+qed "letrecV";
 
 EVal_rls := !EVal_rls @ [letV,letrecV,fixV];
 
diff -r e0e5c1581e4c -r 2ca12511676d src/CCL/ex/List.ML
--- a/src/CCL/ex/List.ML	Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/ex/List.ML	Wed Nov 30 13:53:46 1994 +0100
@@ -34,52 +34,52 @@
 val [prem] = goal List.thy "n:Nat ==> map(f) ^ n ` [] = []";
 br (prem RS Nat_ind) 1;
 by (ALLGOALS (asm_simp_tac list_ss));
-val nmapBnil = result();
+qed "nmapBnil";
 
 val [prem] = goal List.thy "n:Nat ==> map(f)^n`(x$xs) = (f^n`x)$(map(f)^n`xs)";
 br (prem RS Nat_ind) 1;
 by (ALLGOALS (asm_simp_tac list_ss));
-val nmapBcons = result();
+qed "nmapBcons";
 
 (***)
 
 val prems = goalw List.thy [map_def]
   "[| !!x.x:A==>f(x):B;  l : List(A) |] ==> map(f,l) : List(B)";
 by (typechk_tac prems 1);
-val mapT = result();
+qed "mapT";
 
 val prems = goalw List.thy [append_def]
   "[| l : List(A);  m : List(A) |] ==> l @ m : List(A)";
 by (typechk_tac prems 1);
-val appendT = result();
+qed "appendT";
 
 val prems = goal List.thy
   "[| l : {l:List(A). m : {m:List(A).P(l @ m)}} |] ==> l @ m : {x:List(A). P(x)}";
 by (cut_facts_tac prems 1);
 by (fast_tac (set_cs addSIs [SubtypeI,appendT] addSEs [SubtypeE]) 1);
-val appendTS = result();
+qed "appendTS";
 
 val prems = goalw List.thy [filter_def]
   "[| f:A->Bool;   l : List(A) |] ==> filter(f,l) : List(A)";
 by (typechk_tac prems 1);
-val filterT = result();
+qed "filterT";
 
 val prems = goalw List.thy [flat_def]
   "l : List(List(A)) ==> flat(l) : List(A)";
 by (typechk_tac (appendT::prems) 1);
-val flatT = result();
+qed "flatT";
 
 val prems = goalw List.thy [insert_def]
   "[|  f : A->A->Bool; a:A; l : List(A) |] ==> insert(f,a,l) : List(A)";
 by (typechk_tac prems 1);
-val insertT = result();
+qed "insertT";
 
 val prems = goal List.thy
   "[| f : {f:A->A->Bool. a : {a:A. l : {l:List(A).P(insert(f,a,l))}}} |] ==> \
 \  insert(f,a,l)  : {x:List(A). P(x)}";
 by (cut_facts_tac prems 1);
 by (fast_tac (set_cs addSIs [SubtypeI,insertT] addSEs [SubtypeE]) 1);
-val insertTS = result();
+qed "insertTS";
 
 val prems = goalw List.thy [partition_def]
   "[| f:A->Bool;  l : List(A) |] ==> partition(f,l) : List(A)*List(A)";
@@ -88,7 +88,7 @@
 br (ListPRI RS wfstI RS (ListPR_wf RS wmap_wf RS wfI)) 2;
 br (ListPRI RS wfstI RS (ListPR_wf RS wmap_wf RS wfI)) 1;
 by (REPEAT (atac 1));
-val partitionT = result();
+qed "partitionT";
 
 (*** Correctness Conditions for Insertion Sort ***)
 
diff -r e0e5c1581e4c -r 2ca12511676d src/CCL/ex/Nat.ML
--- a/src/CCL/ex/Nat.ML	Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/ex/Nat.ML	Wed Nov 30 13:53:46 1994 +0100
@@ -27,34 +27,34 @@
 val [prem] = goal Nat.thy "n:Nat ==> f^n`f(a) = f^succ(n)`a";
 br (prem RS Nat_ind) 1;
 by (ALLGOALS (asm_simp_tac nat_ss));
-val napply_f = result();
+qed "napply_f";
 
 (****)
 
 val prems = goalw Nat.thy [add_def] "[| a:Nat;  b:Nat |] ==> a #+ b : Nat";
 by (typechk_tac prems 1);
-val addT = result();
+qed "addT";
 
 val prems = goalw Nat.thy [mult_def] "[| a:Nat;  b:Nat |] ==> a #* b : Nat";
 by (typechk_tac (addT::prems) 1);
-val multT = result();
+qed "multT";
 
 (* Defined to return zero if a<b *)
 val prems = goalw Nat.thy [sub_def] "[| a:Nat;  b:Nat |] ==> a #- b : Nat";
 by (typechk_tac (prems) 1);
 by clean_ccs_tac;
 be (NatPRI RS wfstI RS (NatPR_wf RS wmap_wf RS wfI)) 1;
-val subT = result();
+qed "subT";
 
 val prems = goalw Nat.thy [le_def] "[| a:Nat;  b:Nat |] ==> a #<= b : Bool";
 by (typechk_tac (prems) 1);
 by clean_ccs_tac;
 be (NatPRI RS wfstI RS (NatPR_wf RS wmap_wf RS wfI)) 1;
-val leT = result();
+qed "leT";
 
 val prems = goalw Nat.thy [not_def,lt_def] "[| a:Nat;  b:Nat |] ==> a #< b : Bool";
 by (typechk_tac (prems@[leT]) 1);
-val ltT = result();
+qed "ltT";
 
 (* Correctness conditions for subtractive division **)
 
diff -r e0e5c1581e4c -r 2ca12511676d src/CCL/ex/Stream.ML
--- a/src/CCL/ex/Stream.ML	Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/ex/Stream.ML	Wed Nov 30 13:53:46 1994 +0100
@@ -23,7 +23,7 @@
 by (EQgen_tac list_ss [] 1);
 by (simp_tac list_ss 1);
 by (fast_tac ccl_cs 1);
-val map_comp = result();
+qed "map_comp";
 
 (*** Mapping the identity function leaves a list unchanged ***)
 
@@ -35,7 +35,7 @@
 be (XH_to_E ListsXH) 1;
 by (EQgen_tac list_ss [] 1);
 by (fast_tac ccl_cs 1);
-val map_id = result();
+qed "map_id";
 
 (*** Mapping distributes over append ***)
 
@@ -50,7 +50,7 @@
 be (XH_to_E ListsXH) 1;
 by (EQgen_tac list_ss [] 1);
 by (fast_tac ccl_cs 1);
-val map_append = result();
+qed "map_append";
 
 (*** Append is associative ***)
 
@@ -67,7 +67,7 @@
 be (XH_to_E ListsXH) 1;
 by (EQgen_tac list_ss [] 1);
 by (fast_tac ccl_cs 1);
-val append_assoc = result();
+qed "append_assoc";
 
 (*** Appending anything to an infinite list doesn't alter it ****)
 
@@ -78,7 +78,7 @@
 be (XH_to_E IListsXH) 1;
 by (EQgen_tac list_ss [] 1);
 by (fast_tac ccl_cs 1);
-val ilist_append = result();
+qed "ilist_append";
 
 (*** The equivalance of two versions of an iteration function       ***)
 (*                                                                    *)
@@ -88,18 +88,18 @@
 goalw Stream.thy [iter1_def] "iter1(f,a) = a$iter1(f,f(a))";
 br (letrecB RS trans) 1;
 by (simp_tac term_ss 1);
-val iter1B = result();
+qed "iter1B";
 
 goalw Stream.thy [iter2_def] "iter2(f,a) = a $ map(f,iter2(f,a))";
 br (letrecB RS trans) 1;
 br refl 1;
-val iter2B = result();
+qed "iter2B";
 
 val [prem] =goal Stream.thy
    "n:Nat ==> map(f) ^ n ` iter2(f,a) = (f ^ n ` a) $ (map(f) ^ n ` map(f,iter2(f,a)))";
 br (iter2B RS ssubst) 1;back();back();
 by (simp_tac (list_ss addsimps [prem RS nmapBcons]) 1);
-val iter2Blemma = result();
+qed "iter2Blemma";
 
 goal Stream.thy "iter1(f,a) = iter2(f,a)";
 by (eq_coinduct3_tac 
@@ -111,4 +111,4 @@
 by (rtac (napply_f RS ssubst) 1 THEN atac 1);
 by (res_inst_tac [("f1","f")] (napplyBsucc RS subst) 1);
 by (fast_tac type_cs 1);
-val iter1_iter2_eq = result();
+qed "iter1_iter2_eq";
diff -r e0e5c1581e4c -r 2ca12511676d src/CCL/genrec.ML
--- a/src/CCL/genrec.ML	Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/genrec.ML	Wed Nov 30 13:53:46 1994 +0100
@@ -20,12 +20,12 @@
 by (rtac ballI 1);
 by (etac (spec RS mp RS mp) 1);
 by (REPEAT (eresolve_tac [SubtypeD1,SubtypeD2] 1));
-val letrecT = result();
+qed "letrecT";
 
 goalw Wfd.thy [SPLIT_def] "SPLIT(<a,b>,B) = B(a,b)";
 by (rtac set_ext 1);
 by (fast_tac ccl_cs 1);
-val SPLITB = result();
+qed "SPLITB";
 
 val prems = goalw Wfd.thy [letrec2_def]
     "[| a : A;  b : B;  \
@@ -40,11 +40,11 @@
 by (rtac (SPLITB RS subst) 1);
 by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE 
             eresolve_tac [bspec,SubtypeE,sym RS subst] 1));
-val letrec2T = result();
+qed "letrec2T";
 
 goal Wfd.thy "SPLIT(<a,<b,c>>,%x xs.SPLIT(xs,%y z.B(x,y,z))) = B(a,b,c)";
 by (simp_tac (ccl_ss addsimps [SPLITB]) 1);
-val lemma = result();
+qed "lemma";
 
 val prems = goalw Wfd.thy [letrec3_def]
     "[| a : A;  b : B;  c : C;  \
@@ -60,7 +60,7 @@
 by (rtac (lemma RS subst) 1);
 by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE 
             eresolve_tac [bspec,SubtypeE,sym RS subst] 1));
-val letrec3T = result();
+qed "letrec3T";
 
 val letrecTs = [letrecT,letrec2T,letrec3T];
 
@@ -72,14 +72,14 @@
 \       g(a) : D(a) ==> g(a) : E;  a:A;  <a,p>:wf(R) |] ==> \
 \   g(a) : E";
 by (REPEAT (ares_tac ([SubtypeI,major RS bspec,major]@prems) 1));
-val rcallT = result();
+qed "rcallT";
 
 val major::prems = goal Wfd.thy
     "[| ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
 \       g(a,b) : D(a,b) ==> g(a,b) : E;  a:A;  b:B;  <<a,b>,<p,q>>:wf(R) |] ==> \
 \   g(a,b) : E";
 by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec,major]@prems) 1));
-val rcall2T = result();
+qed "rcall2T";
 
 val major::prems = goal Wfd.thy
     "[| ALL x:A.ALL y:B.ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}. g(x,y,z):D(x,y,z); \
@@ -87,7 +87,7 @@
 \       a:A;  b:B;  c:C;  <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==> \
 \   g(a,b,c) : E";
 by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec RS bspec,major]@prems) 1));
-val rcall3T = result();
+qed "rcall3T";
 
 val rcallTs = [rcallT,rcall2T,rcall3T];
 
@@ -113,7 +113,7 @@
 by (resolve_tac (prems RL [sym]) 1);
 by (rtac rcallT 1);
 by (REPEAT (ares_tac prems 1));
-val hyprcallT = result();
+qed "hyprcallT";
 
 val prems = goal Wfd.thy
     "[| g(a,b) = c; ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
@@ -124,7 +124,7 @@
 by (resolve_tac (prems RL [sym]) 1);
 by (rtac rcall2T 1);
 by (REPEAT (ares_tac prems 1));
-val hyprcall2T = result();
+qed "hyprcall2T";
 
 val prems = goal Wfd.thy
   "[| g(a,b,c) = d; \
@@ -136,7 +136,7 @@
 by (resolve_tac (prems RL [sym]) 1);
 by (rtac rcall3T 1);
 by (REPEAT (ares_tac prems 1));
-val hyprcall3T = result();
+qed "hyprcall3T";
 
 val hyprcallTs = [hyprcallT,hyprcall2T,hyprcall3T];
 
@@ -146,20 +146,20 @@
     "[| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); P |] ==> \
 \    P";
 by (REPEAT (ares_tac prems 1));
-val rmIH1  = result();
+qed "rmIH1";
 
 val prems = goal Wfd.thy
     "[| ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P |] ==> \
 \    P";
 by (REPEAT (ares_tac prems 1));
-val rmIH2  = result();
+qed "rmIH2";
 
 val prems = goal Wfd.thy
  "[| ALL x:A.ALL y:B.ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \
 \    P |] ==> \
 \    P";
 by (REPEAT (ares_tac prems 1));
-val rmIH3  = result();
+qed "rmIH3";
 
 val rmIHs = [rmIH1,rmIH2,rmIH3];
 
diff -r e0e5c1581e4c -r 2ca12511676d src/CCL/mono.ML
--- a/src/CCL/mono.ML	Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/mono.ML	Wed Nov 30 13:53:46 1994 +0100
@@ -13,34 +13,34 @@
 
 val prems = goal Set.thy "A<=B ==> Union(A) <= Union(B)";
 by (cfast_tac prems 1);
-val Union_mono = result();
+qed "Union_mono";
 
 val prems = goal Set.thy "[| B<=A |] ==> Inter(A) <= Inter(B)";
 by (cfast_tac prems 1);
-val Inter_anti_mono = result();
+qed "Inter_anti_mono";
 
 val prems = goal Set.thy
     "[| A<=B;  !!x. x:A ==> f(x)<=g(x) |] ==> \
 \    (UN x:A. f(x)) <= (UN x:B. g(x))";
 by (REPEAT (eresolve_tac [UN_E,ssubst] 1
      ORELSE ares_tac ((prems RL [subsetD]) @ [subsetI,UN_I]) 1));
-val UN_mono = result();
+qed "UN_mono";
 
 val prems = goal Set.thy
     "[| B<=A;  !!x. x:A ==> f(x)<=g(x) |] ==> \
 \    (INT x:A. f(x)) <= (INT x:A. g(x))";
 by (REPEAT (ares_tac ((prems RL [subsetD]) @ [subsetI,INT_I]) 1
      ORELSE etac INT_D 1));
-val INT_anti_mono = result();
+qed "INT_anti_mono";
 
 val prems = goal Set.thy "[| A<=C;  B<=D |] ==> A Un B <= C Un D";
 by (cfast_tac prems 1);
-val Un_mono = result();
+qed "Un_mono";
 
 val prems = goal Set.thy "[| A<=C;  B<=D |] ==> A Int B <= C Int D";
 by (cfast_tac prems 1);
-val Int_mono = result();
+qed "Int_mono";
 
 val prems = goal Set.thy "[| A<=B |] ==> Compl(B) <= Compl(A)";
 by (cfast_tac prems 1);
-val Compl_anti_mono = result();
+qed "Compl_anti_mono";
diff -r e0e5c1581e4c -r 2ca12511676d src/CCL/subset.ML
--- a/src/CCL/subset.ML	Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/subset.ML	Wed Nov 30 13:53:46 1994 +0100
@@ -15,13 +15,13 @@
 val prems = goal Set.thy
     "B:A ==> B <= Union(A)";
 by (REPEAT (ares_tac (prems@[subsetI,UnionI]) 1));
-val Union_upper = result();
+qed "Union_upper";
 
 val prems = goal Set.thy
     "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C";
 by (REPEAT (ares_tac [subsetI] 1
      ORELSE eresolve_tac ([UnionE] @ (prems RL [subsetD])) 1));
-val Union_least = result();
+qed "Union_least";
 
 
 (*** Big Intersection -- greatest lower bound of a set ***)
@@ -30,70 +30,70 @@
     "B:A ==> Inter(A) <= B";
 by (REPEAT (resolve_tac (prems@[subsetI]) 1
      ORELSE etac InterD 1));
-val Inter_lower = result();
+qed "Inter_lower";
 
 val prems = goal Set.thy
     "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)";
 by (REPEAT (ares_tac [subsetI,InterI] 1
      ORELSE eresolve_tac (prems RL [subsetD]) 1));
-val Inter_greatest = result();
+qed "Inter_greatest";
 
 (*** Finite Union -- the least upper bound of 2 sets ***)
 
 goal Set.thy "A <= A Un B";
 by (REPEAT (ares_tac [subsetI,UnI1] 1));
-val Un_upper1 = result();
+qed "Un_upper1";
 
 goal Set.thy "B <= A Un B";
 by (REPEAT (ares_tac [subsetI,UnI2] 1));
-val Un_upper2 = result();
+qed "Un_upper2";
 
 val prems = goal Set.thy "[| A<=C;  B<=C |] ==> A Un B <= C";
 by (cut_facts_tac prems 1);
 by (DEPTH_SOLVE (ares_tac [subsetI] 1 
           ORELSE eresolve_tac [UnE,subsetD] 1));
-val Un_least = result();
+qed "Un_least";
 
 (*** Finite Intersection -- the greatest lower bound of 2 sets *)
 
 goal Set.thy "A Int B <= A";
 by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1));
-val Int_lower1 = result();
+qed "Int_lower1";
 
 goal Set.thy "A Int B <= B";
 by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1));
-val Int_lower2 = result();
+qed "Int_lower2";
 
 val prems = goal Set.thy "[| C<=A;  C<=B |] ==> C <= A Int B";
 by (cut_facts_tac prems 1);
 by (REPEAT (ares_tac [subsetI,IntI] 1
      ORELSE etac subsetD 1));
-val Int_greatest = result();
+qed "Int_greatest";
 
 (*** Monotonicity ***)
 
 val [prem] = goalw Set.thy [mono_def]
     "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)";
 by (REPEAT (ares_tac [allI, impI, prem] 1));
-val monoI = result();
+qed "monoI";
 
 val [major,minor] = goalw Set.thy [mono_def]
     "[| mono(f);  A <= B |] ==> f(A) <= f(B)";
 by (rtac (major RS spec RS spec RS mp) 1);
 by (rtac minor 1);
-val monoD = result();
+qed "monoD";
 
 val [prem] = goal Set.thy "mono(f) ==> f(A) Un f(B) <= f(A Un B)";
 by (rtac Un_least 1);
 by (rtac (Un_upper1 RS (prem RS monoD)) 1);
 by (rtac (Un_upper2 RS (prem RS monoD)) 1);
-val mono_Un = result();
+qed "mono_Un";
 
 val [prem] = goal Set.thy "mono(f) ==> f(A Int B) <= f(A) Int f(B)";
 by (rtac Int_greatest 1);
 by (rtac (Int_lower1 RS (prem RS monoD)) 1);
 by (rtac (Int_lower2 RS (prem RS monoD)) 1);
-val mono_Int = result();
+qed "mono_Int";
 
 (****)
 
diff -r e0e5c1581e4c -r 2ca12511676d src/CCL/typecheck.ML
--- a/src/CCL/typecheck.ML	Wed Nov 30 13:18:42 1994 +0100
+++ b/src/CCL/typecheck.ML	Wed Nov 30 13:53:46 1994 +0100
@@ -46,23 +46,23 @@
 by (cut_facts_tac prems 1);
 by (etac (letB RS ssubst) 1);
 by (assume_tac 1);
-val letT = result();
+qed "letT";
 
 val prems = goal Type.thy
      "[| a:A;  f : Pi(A,B)  |] ==> f ` a  : B(a)";
 by (REPEAT (ares_tac (applyT::prems) 1));
-val applyT2 = result();
+qed "applyT2";
 
 val prems = goal Type.thy 
     "[| a:A;  a:A ==> P(a) |] ==> a : {x:A.P(x)}";
 by (fast_tac (type_cs addSIs prems) 1);
-val rcall_lemma1 = result();
+qed "rcall_lemma1";
 
 val prems = goal Type.thy 
     "[| a:{x:A.Q(x)};  [| a:A; Q(a) |] ==> P(a) |] ==> a : {x:A.P(x)}";
 by (cut_facts_tac prems 1);
 by (fast_tac (type_cs addSIs prems) 1);
-val rcall_lemma2 = result();
+qed "rcall_lemma2";
 
 val rcall_lemmas = [asm_rl,rcall_lemma1,SubtypeD1,rcall_lemma2];