added qed and qed_goal[w]
authorclasohm
Wed Nov 30 13:53:46 1994 +0100 (1994-11-30)
changeset 7572ca12511676d
parent 756 e0e5c1581e4c
child 758 c2b210bda710
added qed and qed_goal[w]
src/CCL/CCL.ML
src/CCL/Fix.ML
src/CCL/Gfp.ML
src/CCL/Hered.ML
src/CCL/Lfp.ML
src/CCL/Set.ML
src/CCL/Term.ML
src/CCL/Trancl.ML
src/CCL/Type.ML
src/CCL/Wfd.ML
src/CCL/coinduction.ML
src/CCL/equalities.ML
src/CCL/eval.ML
src/CCL/ex/List.ML
src/CCL/ex/Nat.ML
src/CCL/ex/Stream.ML
src/CCL/genrec.ML
src/CCL/mono.ML
src/CCL/subset.ML
src/CCL/typecheck.ML
     1.1 --- a/src/CCL/CCL.ML	Wed Nov 30 13:18:42 1994 +0100
     1.2 +++ b/src/CCL/CCL.ML	Wed Nov 30 13:53:46 1994 +0100
     1.3 @@ -16,17 +16,17 @@
     1.4  (*** Congruence Rules ***)
     1.5  
     1.6  (*similar to AP_THM in Gordon's HOL*)
     1.7 -val fun_cong = prove_goal CCL.thy "(f::'a=>'b) = g ==> f(x)=g(x)"
     1.8 +qed_goal "fun_cong" CCL.thy "(f::'a=>'b) = g ==> f(x)=g(x)"
     1.9    (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
    1.10  
    1.11  (*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
    1.12 -val arg_cong = prove_goal CCL.thy "x=y ==> f(x)=f(y)"
    1.13 +qed_goal "arg_cong" CCL.thy "x=y ==> f(x)=f(y)"
    1.14   (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
    1.15  
    1.16  goal CCL.thy  "(ALL x. f(x) = g(x)) --> (%x.f(x)) = (%x.g(x))";
    1.17  by (simp_tac (CCL_ss addsimps [eq_iff]) 1);
    1.18  by (fast_tac (set_cs addIs [po_abstractn]) 1);
    1.19 -val abstractn = standard (allI RS (result() RS mp));
    1.20 +val abstractn = store_thm("abstractn", standard (allI RS (result() RS mp)));
    1.21  
    1.22  fun type_of_terms (Const("Trueprop",_) $ 
    1.23                     (Const("op =",(Type ("fun", [t,_]))) $ _ $ _)) = t;
    1.24 @@ -45,18 +45,18 @@
    1.25  
    1.26  goalw CCL.thy [Trm_def,Dvg_def] "Trm(t) <-> ~ t = bot";
    1.27  by (rtac iff_refl 1);
    1.28 -val Trm_iff = result();
    1.29 +qed "Trm_iff";
    1.30  
    1.31  goalw CCL.thy [Trm_def,Dvg_def] "Dvg(t) <-> t = bot";
    1.32  by (rtac iff_refl 1);
    1.33 -val Dvg_iff = result();
    1.34 +qed "Dvg_iff";
    1.35  
    1.36  (*** Constructors are injective ***)
    1.37  
    1.38  val prems = goal CCL.thy
    1.39      "[| x=a;  y=b;  x=y |] ==> a=b";
    1.40  by  (REPEAT (SOMEGOAL (ares_tac (prems@[box_equals]))));
    1.41 -val eq_lemma = result();
    1.42 +qed "eq_lemma";
    1.43  
    1.44  fun mk_inj_rl thy rews s = 
    1.45        let fun mk_inj_lemmas r = ([arg_cong] RL [(r RS (r RS eq_lemma))]);
    1.46 @@ -139,11 +139,11 @@
    1.47  
    1.48  val major::prems = goal Set.thy "[| A=B;  a:B <-> P |] ==> a:A <-> P";
    1.49  by (resolve_tac (prems RL [major RS ssubst]) 1);
    1.50 -val XHlemma1 = result();
    1.51 +qed "XHlemma1";
    1.52  
    1.53  goal CCL.thy "(P(t,t') <-> Q) --> (<t,t'> : {p.EX t t'.p=<t,t'> &  P(t,t')} <-> Q)";
    1.54  by (fast_tac ccl_cs 1);
    1.55 -val XHlemma2 = result() RS mp;
    1.56 +val XHlemma2 = store_thm("XHlemma2", result() RS mp);
    1.57  
    1.58  (*** Pre-Order ***)
    1.59  
    1.60 @@ -153,14 +153,14 @@
    1.61  by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
    1.62  by (ALLGOALS (simp_tac ccl_ss));
    1.63  by (ALLGOALS (fast_tac set_cs));
    1.64 -val POgen_mono = result();
    1.65 +qed "POgen_mono";
    1.66  
    1.67  goalw CCL.thy [POgen_def,SIM_def]
    1.68    "<t,t'> : POgen(R) <-> t= bot | (t=true & t'=true)  | (t=false & t'=false) | \
    1.69  \                    (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
    1.70  \                    (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))";
    1.71  by (rtac (iff_refl RS XHlemma2) 1);
    1.72 -val POgenXH = result();
    1.73 +qed "POgenXH";
    1.74  
    1.75  goal CCL.thy
    1.76    "t [= t' <-> t=bot | (t=true & t'=true) | (t=false & t'=false) | \
    1.77 @@ -170,25 +170,25 @@
    1.78  br (rewrite_rule [POgen_def,SIM_def] 
    1.79                   (POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1;
    1.80  by (rtac (iff_refl RS XHlemma2) 1);
    1.81 -val poXH = result();
    1.82 +qed "poXH";
    1.83  
    1.84  goal CCL.thy "bot [= b";
    1.85  by (rtac (poXH RS iffD2) 1);
    1.86  by (simp_tac ccl_ss 1);
    1.87 -val po_bot = result();
    1.88 +qed "po_bot";
    1.89  
    1.90  goal CCL.thy "a [= bot --> a=bot";
    1.91  by (rtac impI 1);
    1.92  by (dtac (poXH RS iffD1) 1);
    1.93  by (etac rev_mp 1);
    1.94  by (simp_tac ccl_ss 1);
    1.95 -val bot_poleast = result() RS mp;
    1.96 +val bot_poleast = store_thm("bot_poleast", result() RS mp);
    1.97  
    1.98  goal CCL.thy "<a,b> [= <a',b'> <->  a [= a' & b [= b'";
    1.99  by (rtac (poXH RS iff_trans) 1);
   1.100  by (simp_tac ccl_ss 1);
   1.101  by (fast_tac ccl_cs 1);
   1.102 -val po_pair = result();
   1.103 +qed "po_pair";
   1.104  
   1.105  goal CCL.thy "lam x.f(x) [= lam x.f'(x) <-> (ALL x. f(x) [= f'(x))";
   1.106  by (rtac (poXH RS iff_trans) 1);
   1.107 @@ -196,7 +196,7 @@
   1.108  by (REPEAT (ares_tac [iffI,allI] 1 ORELSE eresolve_tac [exE,conjE] 1));
   1.109  by (asm_simp_tac ccl_ss 1);
   1.110  by (fast_tac ccl_cs 1);
   1.111 -val po_lam = result();
   1.112 +qed "po_lam";
   1.113  
   1.114  val ccl_porews = [po_bot,po_pair,po_lam];
   1.115  
   1.116 @@ -210,40 +210,40 @@
   1.117  by (res_inst_tac [("f1","%d.case(t',a',b',c',d)")] 
   1.118                 (p5 RS po_abstractn RS po_cong RS po_trans) 1);
   1.119  by (rtac po_refl 1);
   1.120 -val case_pocong = result();
   1.121 +qed "case_pocong";
   1.122  
   1.123  val [p1,p2] = goalw CCL.thy ccl_data_defs
   1.124      "[| f [= f';  a [= a' |] ==> f ` a [= f' ` a'";
   1.125  by (REPEAT (ares_tac [po_refl,case_pocong,p1,p2 RS po_cong] 1));
   1.126 -val apply_pocong = result();
   1.127 +qed "apply_pocong";
   1.128  
   1.129  
   1.130  val prems = goal CCL.thy "~ lam x.b(x) [= bot";
   1.131  by (rtac notI 1);
   1.132  by (dtac bot_poleast 1);
   1.133  by (etac (distinctness RS notE) 1);
   1.134 -val npo_lam_bot = result();
   1.135 +qed "npo_lam_bot";
   1.136  
   1.137  val eq1::eq2::prems = goal CCL.thy
   1.138      "[| x=a;  y=b;  x[=y |] ==> a[=b";
   1.139  by (rtac (eq1 RS subst) 1);
   1.140  by (rtac (eq2 RS subst) 1);
   1.141  by (resolve_tac prems 1);
   1.142 -val po_lemma = result();
   1.143 +qed "po_lemma";
   1.144  
   1.145  goal CCL.thy "~ <a,b> [= lam x.f(x)";
   1.146  by (rtac notI 1);
   1.147  by (rtac (npo_lam_bot RS notE) 1);
   1.148  by (etac (case_pocong RS (caseBlam RS (caseBpair RS po_lemma))) 1);
   1.149  by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1));
   1.150 -val npo_pair_lam = result();
   1.151 +qed "npo_pair_lam";
   1.152  
   1.153  goal CCL.thy "~ lam x.f(x) [= <a,b>";
   1.154  by (rtac notI 1);
   1.155  by (rtac (npo_lam_bot RS notE) 1);
   1.156  by (etac (case_pocong RS (caseBpair RS (caseBlam RS po_lemma))) 1);
   1.157  by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1));
   1.158 -val npo_lam_pair = result();
   1.159 +qed "npo_lam_pair";
   1.160  
   1.161  fun mk_thm s = prove_goal CCL.thy s (fn _ => 
   1.162                            [rtac notI 1,dtac case_pocong 1,etac rev_mp 5,
   1.163 @@ -262,7 +262,7 @@
   1.164  val prems = goal CCL.thy "[|  <t,u> : R;  R <= POgen(R) |] ==> t [= u";
   1.165  by (rtac (PO_def RS def_coinduct RS (PO_iff RS iffD2)) 1);
   1.166  by (REPEAT (ares_tac prems 1));
   1.167 -val po_coinduct = result();
   1.168 +qed "po_coinduct";
   1.169  
   1.170  fun po_coinduct_tac s i = res_inst_tac [("R",s)] po_coinduct i;
   1.171  
   1.172 @@ -274,7 +274,7 @@
   1.173  by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
   1.174  by (ALLGOALS (simp_tac ccl_ss));
   1.175  by (ALLGOALS (fast_tac set_cs));
   1.176 -val EQgen_mono = result();
   1.177 +qed "EQgen_mono";
   1.178  
   1.179  goalw CCL.thy [EQgen_def,SIM_def]
   1.180    "<t,t'> : EQgen(R) <-> (t=bot & t'=bot)  | (t=true & t'=true)  | \
   1.181 @@ -282,7 +282,7 @@
   1.182  \                (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
   1.183  \                (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))";
   1.184  by (rtac (iff_refl RS XHlemma2) 1);
   1.185 -val EQgenXH = result();
   1.186 +qed "EQgenXH";
   1.187  
   1.188  goal CCL.thy
   1.189    "t=t' <-> (t=bot & t'=bot)  | (t=true & t'=true)  | (t=false & t'=false) | \
   1.190 @@ -297,18 +297,18 @@
   1.191  br (rewrite_rule [EQgen_def,SIM_def]
   1.192                   (EQgen_mono RS (EQ_def RS def_gfp_Tarski) RS XHlemma1)) 1;
   1.193  by (rtac (iff_refl RS XHlemma2) 1);
   1.194 -val eqXH = result();
   1.195 +qed "eqXH";
   1.196  
   1.197  val prems = goal CCL.thy "[|  <t,u> : R;  R <= EQgen(R) |] ==> t = u";
   1.198  by (rtac (EQ_def RS def_coinduct RS (EQ_iff RS iffD2)) 1);
   1.199  by (REPEAT (ares_tac prems 1));
   1.200 -val eq_coinduct = result();
   1.201 +qed "eq_coinduct";
   1.202  
   1.203  val prems = goal CCL.thy 
   1.204      "[|  <t,u> : R;  R <= EQgen(lfp(%x.EQgen(x) Un R Un EQ)) |] ==> t = u";
   1.205  by (rtac (EQ_def RS def_coinduct3 RS (EQ_iff RS iffD2)) 1);
   1.206  by (REPEAT (ares_tac (EQgen_mono::prems) 1));
   1.207 -val eq_coinduct3 = result();
   1.208 +qed "eq_coinduct3";
   1.209  
   1.210  fun eq_coinduct_tac s i = res_inst_tac [("R",s)] eq_coinduct i;
   1.211  fun eq_coinduct3_tac s i = res_inst_tac [("R",s)] eq_coinduct3 i;
   1.212 @@ -318,17 +318,17 @@
   1.213  goalw CCL.thy [apply_def]  "(EX f.t=lam x.f(x)) --> t = lam x.(t ` x)";
   1.214  by (safe_tac ccl_cs);
   1.215  by (simp_tac ccl_ss 1);
   1.216 -val cond_eta = result() RS mp;
   1.217 +val cond_eta = store_thm("cond_eta", result() RS mp);
   1.218  
   1.219  goal CCL.thy "(t=bot) | (t=true) | (t=false) | (EX a b.t=<a,b>) | (EX f.t=lam x.f(x))";
   1.220  by (cut_facts_tac [refl RS (eqXH RS iffD1)] 1);
   1.221  by (fast_tac set_cs 1);
   1.222 -val exhaustion = result();
   1.223 +qed "exhaustion";
   1.224  
   1.225  val prems = goal CCL.thy 
   1.226      "[| P(bot);  P(true);  P(false);  !!x y.P(<x,y>);  !!b.P(lam x.b(x)) |] ==> P(t)";
   1.227  by (cut_facts_tac [exhaustion] 1);
   1.228  by (REPEAT_SOME (ares_tac prems ORELSE' eresolve_tac [disjE,exE,ssubst]));
   1.229 -val term_case = result();
   1.230 +qed "term_case";
   1.231  
   1.232  fun term_case_tac a i = res_inst_tac [("t",a)] term_case i;
     2.1 --- a/src/CCL/Fix.ML	Wed Nov 30 13:18:42 1994 +0100
     2.2 +++ b/src/CCL/Fix.ML	Wed Nov 30 13:53:46 1994 +0100
     2.3 @@ -16,30 +16,30 @@
     2.4  by (rtac (Nat_ind RS ballI) 1 THEN atac 1);
     2.5  by (ALLGOALS (simp_tac term_ss));
     2.6  by (REPEAT (ares_tac [base,step] 1));
     2.7 -val fix_ind = result();
     2.8 +qed "fix_ind";
     2.9  
    2.10  (*** Inclusive Predicates ***)
    2.11  
    2.12  val prems = goalw Fix.thy [INCL_def]
    2.13       "INCL(P) <-> (ALL f. (ALL n:Nat. P(f ^ n ` bot)) --> P(fix(f)))";
    2.14  by (rtac iff_refl 1);
    2.15 -val inclXH = result();
    2.16 +qed "inclXH";
    2.17  
    2.18  val prems = goal Fix.thy
    2.19       "[| !!f.ALL n:Nat.P(f^n`bot) ==> P(fix(f)) |] ==> INCL(%x.P(x))";
    2.20  by (fast_tac (term_cs addIs (prems @ [XH_to_I inclXH])) 1);
    2.21 -val inclI = result();
    2.22 +qed "inclI";
    2.23  
    2.24  val incl::prems = goal Fix.thy
    2.25       "[| INCL(P);  !!n.n:Nat ==> P(f^n`bot) |] ==> P(fix(f))";
    2.26  by (fast_tac (term_cs addIs ([ballI RS (incl RS (XH_to_D inclXH) RS spec RS mp)] 
    2.27                         @ prems)) 1);
    2.28 -val inclD = result();
    2.29 +qed "inclD";
    2.30  
    2.31  val incl::prems = goal Fix.thy
    2.32       "[| INCL(P);  (ALL n:Nat.P(f^n`bot))-->P(fix(f)) ==> R |] ==> R";
    2.33  by (fast_tac (term_cs addIs ([incl RS inclD] @ prems)) 1);
    2.34 -val inclE = result();
    2.35 +qed "inclE";
    2.36  
    2.37  
    2.38  (*** Lemmas for Inclusive Predicates ***)
    2.39 @@ -53,24 +53,24 @@
    2.40  by (assume_tac 2);
    2.41  by (rtac (napplyBzero RS ssubst) 1);
    2.42  by (rtac po_cong 1 THEN rtac po_bot 1);
    2.43 -val npo_INCL = result();
    2.44 +qed "npo_INCL";
    2.45  
    2.46  val prems = goal Fix.thy "[| INCL(P);  INCL(Q) |] ==> INCL(%x.P(x) & Q(x))";
    2.47  by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
    2.48 -val conj_INCL = result();
    2.49 +qed "conj_INCL";
    2.50  
    2.51  val prems = goal Fix.thy "[| !!a.INCL(P(a)) |] ==> INCL(%x.ALL a.P(a,x))";
    2.52  by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
    2.53 -val all_INCL = result();
    2.54 +qed "all_INCL";
    2.55  
    2.56  val prems = goal Fix.thy "[| !!a.a:A ==> INCL(P(a)) |] ==> INCL(%x.ALL a:A.P(a,x))";
    2.57  by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
    2.58 -val ball_INCL = result();
    2.59 +qed "ball_INCL";
    2.60  
    2.61  goal Fix.thy "INCL(%x.a(x) = (b(x)::'a::prog))";
    2.62  by (simp_tac (term_ss addsimps [eq_iff]) 1);
    2.63  by (REPEAT (resolve_tac [conj_INCL,po_INCL] 1));
    2.64 -val eq_INCL = result();
    2.65 +qed "eq_INCL";
    2.66  
    2.67  (*** Derivation of Reachability Condition ***)
    2.68  
    2.69 @@ -78,13 +78,13 @@
    2.70  
    2.71  goal Fix.thy "idgen(fix(idgen)) = fix(idgen)";
    2.72  by (rtac (fixB RS sym) 1);
    2.73 -val fix_idgenfp = result();
    2.74 +qed "fix_idgenfp";
    2.75  
    2.76  goalw Fix.thy [idgen_def] "idgen(lam x.x) = lam x.x";
    2.77  by (simp_tac term_ss 1);
    2.78  by (rtac (term_case RS allI) 1);
    2.79  by (ALLGOALS (simp_tac term_ss));
    2.80 -val id_idgenfp = result();
    2.81 +qed "id_idgenfp";
    2.82  
    2.83  (* All fixed points are lam-expressions *)
    2.84  
    2.85 @@ -92,14 +92,14 @@
    2.86  by (rtac (prem RS subst) 1);
    2.87  by (rewtac idgen_def);
    2.88  by (rtac refl 1);
    2.89 -val idgenfp_lam = result();
    2.90 +qed "idgenfp_lam";
    2.91  
    2.92  (* Lemmas for rewriting fixed points of idgen *)
    2.93  
    2.94  val prems = goalw Fix.thy [idgen_def] 
    2.95      "[| a = b;  a ` t = u |] ==> b ` t = u";
    2.96  by (simp_tac (term_ss addsimps (prems RL [sym])) 1);
    2.97 -val l_lemma= result();
    2.98 +qed "l_lemma";
    2.99  
   2.100  val idgen_lemmas =
   2.101      let fun mk_thm s = prove_goalw Fix.thy [idgen_def] s
   2.102 @@ -120,12 +120,12 @@
   2.103  by (rtac (p2 RS cond_eta RS ssubst) 1);
   2.104  by (rtac (p3 RS cond_eta RS ssubst) 1);
   2.105  by (rtac (p1 RS (po_lam RS iffD2)) 1);
   2.106 -val po_eta = result();
   2.107 +qed "po_eta";
   2.108  
   2.109  val [prem] = goalw Fix.thy [idgen_def] "idgen(d) = d ==> d = lam x.?f(x)";
   2.110  by (rtac (prem RS subst) 1);
   2.111  by (rtac refl 1);
   2.112 -val po_eta_lemma = result();
   2.113 +qed "po_eta_lemma";
   2.114  
   2.115  val [prem] = goal Fix.thy
   2.116      "idgen(d) = d ==> \
   2.117 @@ -135,14 +135,14 @@
   2.118  by (term_case_tac "t" 1);
   2.119  by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem,fix_idgenfp] RL idgen_lemmas)))));
   2.120  by (ALLGOALS (fast_tac set_cs));
   2.121 -val lemma1 = result();
   2.122 +qed "lemma1";
   2.123  
   2.124  val [prem] = goal Fix.thy
   2.125      "idgen(d) = d ==> fix(idgen) [= d";
   2.126  by (rtac (allI RS po_eta) 1);
   2.127  by (rtac (lemma1 RSN(2,po_coinduct)) 1);
   2.128  by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp])));
   2.129 -val fix_least_idgen = result();
   2.130 +qed "fix_least_idgen";
   2.131  
   2.132  val [prem] = goal Fix.thy
   2.133      "idgen(d) = d ==> \
   2.134 @@ -151,7 +151,7 @@
   2.135  by (term_case_tac "a" 1);
   2.136  by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem] RL idgen_lemmas)))));
   2.137  by (ALLGOALS (fast_tac set_cs));
   2.138 -val lemma2 = result();
   2.139 +qed "lemma2";
   2.140  
   2.141  val [prem] = goal Fix.thy
   2.142      "idgen(d) = d ==> lam x.x [= d";
   2.143 @@ -159,20 +159,20 @@
   2.144  by (rtac (lemma2 RSN(2,po_coinduct)) 1);
   2.145  by (simp_tac term_ss 1);
   2.146  by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp])));
   2.147 -val id_least_idgen = result();
   2.148 +qed "id_least_idgen";
   2.149  
   2.150  goal Fix.thy  "fix(idgen) = lam x.x";
   2.151  by (fast_tac (term_cs addIs [eq_iff RS iffD2,
   2.152                               id_idgenfp RS fix_least_idgen,
   2.153                               fix_idgenfp RS id_least_idgen]) 1);
   2.154 -val reachability = result();
   2.155 +qed "reachability";
   2.156  
   2.157  (********)
   2.158  
   2.159  val [prem] = goal Fix.thy "f = lam x.x ==> f`t = t";
   2.160  by (rtac (prem RS sym RS subst) 1);
   2.161  by (rtac applyB 1);
   2.162 -val id_apply = result();
   2.163 +qed "id_apply";
   2.164  
   2.165  val prems = goal Fix.thy
   2.166       "[| P(bot);  P(true);  P(false);  \
   2.167 @@ -190,5 +190,5 @@
   2.168  by (res_inst_tac [("t","xa")] term_case 1);
   2.169  by (ALLGOALS (simp_tac term_ss));
   2.170  by (ALLGOALS (fast_tac (term_cs addIs ([all_INCL,INCL_subst] @ prems))));
   2.171 -val term_ind = result();
   2.172 +qed "term_ind";
   2.173  
     3.1 --- a/src/CCL/Gfp.ML	Wed Nov 30 13:18:42 1994 +0100
     3.2 +++ b/src/CCL/Gfp.ML	Wed Nov 30 13:53:46 1994 +0100
     3.3 @@ -18,27 +18,27 @@
     3.4  val prems = goalw Gfp.thy [gfp_def] "[| A <= f(A) |] ==> A <= gfp(f)";
     3.5  by (rtac (CollectI RS Union_upper) 1);
     3.6  by (resolve_tac prems 1);
     3.7 -val gfp_upperbound = result();
     3.8 +qed "gfp_upperbound";
     3.9  
    3.10  val prems = goalw Gfp.thy [gfp_def]
    3.11      "[| !!u. u <= f(u) ==> u<=A |] ==> gfp(f) <= A";
    3.12  by (REPEAT (ares_tac ([Union_least]@prems) 1));
    3.13  by (etac CollectD 1);
    3.14 -val gfp_least = result();
    3.15 +qed "gfp_least";
    3.16  
    3.17  val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) <= f(gfp(f))";
    3.18  by (EVERY1 [rtac gfp_least, rtac subset_trans, atac,
    3.19  	    rtac (mono RS monoD), rtac gfp_upperbound, atac]);
    3.20 -val gfp_lemma2 = result();
    3.21 +qed "gfp_lemma2";
    3.22  
    3.23  val [mono] = goal Gfp.thy "mono(f) ==> f(gfp(f)) <= gfp(f)";
    3.24  by (EVERY1 [rtac gfp_upperbound, rtac (mono RS monoD), 
    3.25  	    rtac gfp_lemma2, rtac mono]);
    3.26 -val gfp_lemma3 = result();
    3.27 +qed "gfp_lemma3";
    3.28  
    3.29  val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) = f(gfp(f))";
    3.30  by (REPEAT (resolve_tac [equalityI,gfp_lemma2,gfp_lemma3,mono] 1));
    3.31 -val gfp_Tarski = result();
    3.32 +qed "gfp_Tarski";
    3.33  
    3.34  (*** Coinduction rules for greatest fixed points ***)
    3.35  
    3.36 @@ -47,7 +47,7 @@
    3.37      "[| a: A;  A <= f(A) |] ==> a : gfp(f)";
    3.38  by (rtac (gfp_upperbound RS subsetD) 1);
    3.39  by (REPEAT (ares_tac prems 1));
    3.40 -val coinduct = result();
    3.41 +qed "coinduct";
    3.42  
    3.43  val [prem,mono] = goal Gfp.thy
    3.44      "[| A <= f(A) Un gfp(f);  mono(f) |] ==>  \
    3.45 @@ -57,7 +57,7 @@
    3.46  by (rtac (mono RS gfp_Tarski RS subst) 1);
    3.47  by (rtac (prem RS Un_least) 1);
    3.48  by (rtac Un_upper2 1);
    3.49 -val coinduct2_lemma = result();
    3.50 +qed "coinduct2_lemma";
    3.51  
    3.52  (*strong version, thanks to Martin Coen*)
    3.53  val ainA::prems = goal Gfp.thy
    3.54 @@ -65,7 +65,7 @@
    3.55  by (rtac coinduct 1);
    3.56  by (rtac (prems MRS coinduct2_lemma) 2);
    3.57  by (resolve_tac [ainA RS UnI1] 1);
    3.58 -val coinduct2 = result();
    3.59 +qed "coinduct2";
    3.60  
    3.61  (***  Even Stronger version of coinduct  [by Martin Coen]
    3.62           - instead of the condition  A <= f(A)
    3.63 @@ -73,7 +73,7 @@
    3.64  
    3.65  val [prem] = goal Gfp.thy "mono(f) ==> mono(%x.f(x) Un A Un B)";
    3.66  by (REPEAT (ares_tac [subset_refl, monoI, Un_mono, prem RS monoD] 1));
    3.67 -val coinduct3_mono_lemma= result();
    3.68 +qed "coinduct3_mono_lemma";
    3.69  
    3.70  val [prem,mono] = goal Gfp.thy
    3.71      "[| A <= f(lfp(%x.f(x) Un A Un gfp(f)));  mono(f) |] ==> \
    3.72 @@ -87,7 +87,7 @@
    3.73  by (rtac (mono RS monoD) 1);
    3.74  by (rtac (mono RS coinduct3_mono_lemma RS lfp_Tarski RS ssubst) 1);
    3.75  by (rtac Un_upper2 1);
    3.76 -val coinduct3_lemma = result();
    3.77 +qed "coinduct3_lemma";
    3.78  
    3.79  val ainA::prems = goal Gfp.thy
    3.80      "[| a:A;  A <= f(lfp(%x.f(x) Un A Un gfp(f))); mono(f) |] ==> a : gfp(f)";
    3.81 @@ -95,7 +95,7 @@
    3.82  by (rtac (prems MRS coinduct3_lemma) 2);
    3.83  by (resolve_tac (prems RL [coinduct3_mono_lemma RS lfp_Tarski RS ssubst]) 1);
    3.84  by (rtac (ainA RS UnI2 RS UnI1) 1);
    3.85 -val coinduct3 = result();
    3.86 +qed "coinduct3";
    3.87  
    3.88  
    3.89  (** Definition forms of gfp_Tarski, to control unfolding **)
    3.90 @@ -103,25 +103,25 @@
    3.91  val [rew,mono] = goal Gfp.thy "[| h==gfp(f);  mono(f) |] ==> h = f(h)";
    3.92  by (rewtac rew);
    3.93  by (rtac (mono RS gfp_Tarski) 1);
    3.94 -val def_gfp_Tarski = result();
    3.95 +qed "def_gfp_Tarski";
    3.96  
    3.97  val rew::prems = goal Gfp.thy
    3.98      "[| h==gfp(f);  a:A;  A <= f(A) |] ==> a: h";
    3.99  by (rewtac rew);
   3.100  by (REPEAT (ares_tac (prems @ [coinduct]) 1));
   3.101 -val def_coinduct = result();
   3.102 +qed "def_coinduct";
   3.103  
   3.104  val rew::prems = goal Gfp.thy
   3.105      "[| h==gfp(f);  a:A;  A <= f(A) Un h; mono(f) |] ==> a: h";
   3.106  by (rewtac rew);
   3.107  by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct2]) 1));
   3.108 -val def_coinduct2 = result();
   3.109 +qed "def_coinduct2";
   3.110  
   3.111  val rew::prems = goal Gfp.thy
   3.112      "[| h==gfp(f);  a:A;  A <= f(lfp(%x.f(x) Un A Un h)); mono(f) |] ==> a: h";
   3.113  by (rewtac rew);
   3.114  by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct3]) 1));
   3.115 -val def_coinduct3 = result();
   3.116 +qed "def_coinduct3";
   3.117  
   3.118  (*Monotonicity of gfp!*)
   3.119  val prems = goal Gfp.thy
   3.120 @@ -131,4 +131,4 @@
   3.121  by (rtac gfp_lemma2 1);
   3.122  by (resolve_tac prems 1);
   3.123  by (resolve_tac prems 1);
   3.124 -val gfp_mono = result();
   3.125 +qed "gfp_mono";
     4.1 --- a/src/CCL/Hered.ML	Wed Nov 30 13:18:42 1994 +0100
     4.2 +++ b/src/CCL/Hered.ML	Wed Nov 30 13:53:46 1994 +0100
     4.3 @@ -15,13 +15,13 @@
     4.4  goalw Hered.thy [HTTgen_def]  "mono(%X.HTTgen(X))";
     4.5  by (rtac monoI 1);
     4.6  by (fast_tac set_cs 1);
     4.7 -val HTTgen_mono = result();
     4.8 +qed "HTTgen_mono";
     4.9  
    4.10  goalw Hered.thy [HTTgen_def]
    4.11    "t : HTTgen(A) <-> t=true | t=false | (EX a b.t=<a,b> & a : A & b : A) | \
    4.12  \                                       (EX f.t=lam x.f(x) & (ALL x.f(x) : A))";
    4.13  by (fast_tac set_cs 1);
    4.14 -val HTTgenXH = result();
    4.15 +qed "HTTgenXH";
    4.16  
    4.17  goal Hered.thy
    4.18    "t : HTT <-> t=true | t=false | (EX a b.t=<a,b> & a : HTT & b : HTT) | \
    4.19 @@ -29,26 +29,26 @@
    4.20  br (rewrite_rule [HTTgen_def] 
    4.21                   (HTTgen_mono RS (HTT_def RS def_gfp_Tarski) RS XHlemma1)) 1;
    4.22  by (fast_tac set_cs 1);
    4.23 -val HTTXH = result();
    4.24 +qed "HTTXH";
    4.25  
    4.26  (*** Introduction Rules for HTT ***)
    4.27  
    4.28  goal Hered.thy "~ bot : HTT";
    4.29  by (fast_tac (term_cs addDs [XH_to_D HTTXH]) 1);
    4.30 -val HTT_bot = result();
    4.31 +qed "HTT_bot";
    4.32  
    4.33  goal Hered.thy "true : HTT";
    4.34  by (fast_tac (term_cs addIs [XH_to_I HTTXH]) 1);
    4.35 -val HTT_true = result();
    4.36 +qed "HTT_true";
    4.37  
    4.38  goal Hered.thy "false : HTT";
    4.39  by (fast_tac (term_cs addIs [XH_to_I HTTXH]) 1);
    4.40 -val HTT_false = result();
    4.41 +qed "HTT_false";
    4.42  
    4.43  goal Hered.thy "<a,b> : HTT <->  a : HTT  & b : HTT";
    4.44  by (rtac (HTTXH RS iff_trans) 1);
    4.45  by (fast_tac term_cs 1);
    4.46 -val HTT_pair = result();
    4.47 +qed "HTT_pair";
    4.48  
    4.49  goal Hered.thy "lam x.f(x) : HTT <-> (ALL x. f(x) : HTT)";
    4.50  by (rtac (HTTXH RS iff_trans) 1);
    4.51 @@ -56,7 +56,7 @@
    4.52  by (safe_tac term_cs);
    4.53  by (asm_simp_tac term_ss 1);
    4.54  by (fast_tac term_cs 1);
    4.55 -val HTT_lam = result();
    4.56 +qed "HTT_lam";
    4.57  
    4.58  local
    4.59    val raw_HTTrews = [HTT_bot,HTT_true,HTT_false,HTT_pair,HTT_lam];
    4.60 @@ -80,7 +80,7 @@
    4.61  val prems = goal Hered.thy "[|  t : R;  R <= HTTgen(R) |] ==> t : HTT";
    4.62  by (rtac (HTT_def RS def_coinduct) 1);
    4.63  by (REPEAT (ares_tac prems 1));
    4.64 -val HTT_coinduct = result();
    4.65 +qed "HTT_coinduct";
    4.66  
    4.67  fun HTT_coinduct_tac s i = res_inst_tac [("R",s)] HTT_coinduct i;
    4.68  
    4.69 @@ -88,7 +88,7 @@
    4.70      "[|  t : R;   R <= HTTgen(lfp(%x. HTTgen(x) Un R Un HTT)) |] ==> t : HTT";
    4.71  by (rtac (HTTgen_mono RSN(3,HTT_def RS def_coinduct3)) 1);
    4.72  by (REPEAT (ares_tac prems 1));
    4.73 -val HTT_coinduct3 = result();
    4.74 +qed "HTT_coinduct3";
    4.75  val HTT_coinduct3_raw = rewrite_rule [HTTgen_def] HTT_coinduct3;
    4.76  
    4.77  fun HTT_coinduct3_tac s i = res_inst_tac [("R",s)] HTT_coinduct3 i;
    4.78 @@ -114,23 +114,23 @@
    4.79  
    4.80  goal Hered.thy "Unit <= HTT";
    4.81  by (simp_tac (CCL_ss addsimps ([subsetXH,UnitXH] @ HTT_rews)) 1);
    4.82 -val UnitF = result();
    4.83 +qed "UnitF";
    4.84  
    4.85  goal Hered.thy "Bool <= HTT";
    4.86  by (simp_tac (CCL_ss addsimps ([subsetXH,BoolXH] @ HTT_rews)) 1);
    4.87  by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
    4.88 -val BoolF = result();
    4.89 +qed "BoolF";
    4.90  
    4.91  val prems = goal Hered.thy "[| A <= HTT;  B <= HTT |] ==> A + B  <= HTT";
    4.92  by (simp_tac (CCL_ss addsimps ([subsetXH,PlusXH] @ HTT_rews)) 1);
    4.93  by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
    4.94 -val PlusF = result();
    4.95 +qed "PlusF";
    4.96  
    4.97  val prems = goal Hered.thy 
    4.98       "[| A <= HTT;  !!x.x:A ==> B(x) <= HTT |] ==> SUM x:A.B(x) <= HTT";
    4.99  by (simp_tac (CCL_ss addsimps ([subsetXH,SgXH] @ HTT_rews)) 1);
   4.100  by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
   4.101 -val SigmaF = result();
   4.102 +qed "SigmaF";
   4.103  
   4.104  (*** Formation Rules for Recursive types - using coinduction these only need ***)
   4.105  (***                                          exhaution rule for type-former ***)
   4.106 @@ -148,7 +148,7 @@
   4.107  by (etac HTT_coinduct3 1);
   4.108  by (fast_tac (set_cs addIs HTTgenIs 
   4.109                   addSEs [HTTgen_mono RS ci3_RI] addEs [XH_to_E NatXH]) 1);
   4.110 -val NatF = result();
   4.111 +qed "NatF";
   4.112  
   4.113  val [prem] = goal Hered.thy "A <= HTT ==> List(A) <= HTT";
   4.114  by (safe_tac set_cs);
   4.115 @@ -156,7 +156,7 @@
   4.116  by (fast_tac (set_cs addSIs HTTgenIs 
   4.117                   addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] 
   4.118                   addEs [XH_to_E ListXH]) 1);
   4.119 -val ListF = result();
   4.120 +qed "ListF";
   4.121  
   4.122  val [prem] = goal Hered.thy "A <= HTT ==> Lists(A) <= HTT";
   4.123  by (safe_tac set_cs);
   4.124 @@ -164,7 +164,7 @@
   4.125  by (fast_tac (set_cs addSIs HTTgenIs 
   4.126                   addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] 
   4.127                   addEs [XH_to_E ListsXH]) 1);
   4.128 -val ListsF = result();
   4.129 +qed "ListsF";
   4.130  
   4.131  val [prem] = goal Hered.thy "A <= HTT ==> ILists(A) <= HTT";
   4.132  by (safe_tac set_cs);
   4.133 @@ -172,7 +172,7 @@
   4.134  by (fast_tac (set_cs addSIs HTTgenIs 
   4.135                   addSEs [HTTgen_mono RS ci3_RI,prem RS subsetD RS (HTTgen_mono RS ci3_AI)] 
   4.136                   addEs [XH_to_E IListsXH]) 1);
   4.137 -val IListsF = result();
   4.138 +qed "IListsF";
   4.139  
   4.140  (*** A possible use for this predicate is proving equality from pre-order       ***)
   4.141  (*** but it seems as easy (and more general) to do this directly by coinduction ***)
   4.142 @@ -186,9 +186,9 @@
   4.143  by (REPEAT_SOME (rtac (POgenXH RS iffD2) ORELSE' etac rev_mp));
   4.144  by (ALLGOALS (simp_tac (term_ss addsimps HTT_rews)));
   4.145  by (ALLGOALS (fast_tac ccl_cs));
   4.146 -val HTT_po_op = result();
   4.147 +qed "HTT_po_op";
   4.148  
   4.149  val prems = goal Hered.thy "[| t : HTT;  t [= u |] ==> t = u";
   4.150  by (REPEAT (ares_tac (prems @ [conjI RS (eq_iff RS iffD2),HTT_po_op]) 1));
   4.151 -val HTT_po_eq = result();
   4.152 +qed "HTT_po_eq";
   4.153  *)
     5.1 --- a/src/CCL/Lfp.ML	Wed Nov 30 13:18:42 1994 +0100
     5.2 +++ b/src/CCL/Lfp.ML	Wed Nov 30 13:53:46 1994 +0100
     5.3 @@ -18,27 +18,27 @@
     5.4  val prems = goalw Lfp.thy [lfp_def] "[| f(A) <= A |] ==> lfp(f) <= A";
     5.5  by (rtac (CollectI RS Inter_lower) 1);
     5.6  by (resolve_tac prems 1);
     5.7 -val lfp_lowerbound = result();
     5.8 +qed "lfp_lowerbound";
     5.9  
    5.10  val prems = goalw Lfp.thy [lfp_def]
    5.11      "[| !!u. f(u) <= u ==> A<=u |] ==> A <= lfp(f)";
    5.12  by (REPEAT (ares_tac ([Inter_greatest]@prems) 1));
    5.13  by (etac CollectD 1);
    5.14 -val lfp_greatest = result();
    5.15 +qed "lfp_greatest";
    5.16  
    5.17  val [mono] = goal Lfp.thy "mono(f) ==> f(lfp(f)) <= lfp(f)";
    5.18  by (EVERY1 [rtac lfp_greatest, rtac subset_trans,
    5.19  	    rtac (mono RS monoD), rtac lfp_lowerbound, atac, atac]);
    5.20 -val lfp_lemma2 = result();
    5.21 +qed "lfp_lemma2";
    5.22  
    5.23  val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) <= f(lfp(f))";
    5.24  by (EVERY1 [rtac lfp_lowerbound, rtac (mono RS monoD), 
    5.25  	    rtac lfp_lemma2, rtac mono]);
    5.26 -val lfp_lemma3 = result();
    5.27 +qed "lfp_lemma3";
    5.28  
    5.29  val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) = f(lfp(f))";
    5.30  by (REPEAT (resolve_tac [equalityI,lfp_lemma2,lfp_lemma3,mono] 1));
    5.31 -val lfp_Tarski = result();
    5.32 +qed "lfp_Tarski";
    5.33  
    5.34  
    5.35  (*** General induction rule for least fixed points ***)
    5.36 @@ -53,14 +53,14 @@
    5.37  	    rtac (Int_lower1 RS (mono RS monoD)),
    5.38  	    rtac (mono RS lfp_lemma2),
    5.39  	    rtac (CollectI RS subsetI), rtac indhyp, atac]);
    5.40 -val induct = result();
    5.41 +qed "induct";
    5.42  
    5.43  (** Definition forms of lfp_Tarski and induct, to control unfolding **)
    5.44  
    5.45  val [rew,mono] = goal Lfp.thy "[| h==lfp(f);  mono(f) |] ==> h = f(h)";
    5.46  by (rewtac rew);
    5.47  by (rtac (mono RS lfp_Tarski) 1);
    5.48 -val def_lfp_Tarski = result();
    5.49 +qed "def_lfp_Tarski";
    5.50  
    5.51  val rew::prems = goal Lfp.thy
    5.52      "[| A == lfp(f);  a:A;  mono(f);   			\
    5.53 @@ -68,7 +68,7 @@
    5.54  \    |] ==> P(a)";
    5.55  by (EVERY1 [rtac induct,	(*backtracking to force correct induction*)
    5.56  	    REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]);
    5.57 -val def_induct = result();
    5.58 +qed "def_induct";
    5.59  
    5.60  (*Monotonicity of lfp!*)
    5.61  val prems = goal Lfp.thy
    5.62 @@ -78,5 +78,5 @@
    5.63  by (resolve_tac prems 1);
    5.64  by (rtac lfp_lemma2 1);
    5.65  by (resolve_tac prems 1);
    5.66 -val lfp_mono = result();
    5.67 +qed "lfp_mono";
    5.68  
     6.1 --- a/src/CCL/Set.ML	Wed Nov 30 13:18:42 1994 +0100
     6.2 +++ b/src/CCL/Set.ML	Wed Nov 30 13:53:46 1994 +0100
     6.3 @@ -16,36 +16,36 @@
     6.4  val [prem] = goal Set.thy "[| P(a) |] ==> a : {x.P(x)}";
     6.5  by (rtac (mem_Collect_iff RS iffD2) 1);
     6.6  by (rtac prem 1);
     6.7 -val CollectI = result();
     6.8 +qed "CollectI";
     6.9  
    6.10  val prems = goal Set.thy "[| a : {x.P(x)} |] ==> P(a)";
    6.11  by (resolve_tac (prems RL [mem_Collect_iff  RS iffD1]) 1);
    6.12 -val CollectD = result();
    6.13 +qed "CollectD";
    6.14  
    6.15  val CollectE = make_elim CollectD;
    6.16  
    6.17  val [prem] = goal Set.thy "[| !!x. x:A <-> x:B |] ==> A = B";
    6.18  by (rtac (set_extension RS iffD2) 1);
    6.19  by (rtac (prem RS allI) 1);
    6.20 -val set_ext = result();
    6.21 +qed "set_ext";
    6.22  
    6.23  (*** Bounded quantifiers ***)
    6.24  
    6.25  val prems = goalw Set.thy [Ball_def]
    6.26      "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)";
    6.27  by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
    6.28 -val ballI = result();
    6.29 +qed "ballI";
    6.30  
    6.31  val [major,minor] = goalw Set.thy [Ball_def]
    6.32      "[| ALL x:A. P(x);  x:A |] ==> P(x)";
    6.33  by (rtac (minor RS (major RS spec RS mp)) 1);
    6.34 -val bspec = result();
    6.35 +qed "bspec";
    6.36  
    6.37  val major::prems = goalw Set.thy [Ball_def]
    6.38      "[| ALL x:A. P(x);  P(x) ==> Q;  ~ x:A ==> Q |] ==> Q";
    6.39  by (rtac (major RS spec RS impCE) 1);
    6.40  by (REPEAT (eresolve_tac prems 1));
    6.41 -val ballE = result();
    6.42 +qed "ballE";
    6.43  
    6.44  (*Takes assumptions ALL x:A.P(x) and a:A; creates assumption P(a)*)
    6.45  fun ball_tac i = etac ballE i THEN contr_tac (i+1);
    6.46 @@ -53,9 +53,9 @@
    6.47  val prems = goalw Set.thy [Bex_def]
    6.48      "[| P(x);  x:A |] ==> EX x:A. P(x)";
    6.49  by (REPEAT (ares_tac (prems @ [exI,conjI]) 1));
    6.50 -val bexI = result();
    6.51 +qed "bexI";
    6.52  
    6.53 -val bexCI = prove_goal Set.thy 
    6.54 +qed_goal "bexCI" Set.thy 
    6.55     "[| EX x:A. ~P(x) ==> P(a);  a:A |] ==> EX x:A.P(x)"
    6.56   (fn prems=>
    6.57    [ (rtac classical 1),
    6.58 @@ -65,13 +65,13 @@
    6.59      "[| EX x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q  |] ==> Q";
    6.60  by (rtac (major RS exE) 1);
    6.61  by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1));
    6.62 -val bexE = result();
    6.63 +qed "bexE";
    6.64  
    6.65  (*Trival rewrite rule;   (! x:A.P)=P holds only if A is nonempty!*)
    6.66  val prems = goal Set.thy
    6.67      "(ALL x:A. True) <-> True";
    6.68  by (REPEAT (ares_tac [TrueI,ballI,iffI] 1));
    6.69 -val ball_rew = result();
    6.70 +qed "ball_rew";
    6.71  
    6.72  (** Congruence rules **)
    6.73  
    6.74 @@ -81,7 +81,7 @@
    6.75  by (resolve_tac (prems RL [ssubst,iffD2]) 1);
    6.76  by (REPEAT (ares_tac [ballI,iffI] 1
    6.77       ORELSE eresolve_tac ([make_elim bspec, mp] @ (prems RL [iffE])) 1));
    6.78 -val ball_cong = result();
    6.79 +qed "ball_cong";
    6.80  
    6.81  val prems = goal Set.thy
    6.82      "[| A=A';  !!x. x:A' ==> P(x) <-> P'(x) |] ==> \
    6.83 @@ -89,37 +89,37 @@
    6.84  by (resolve_tac (prems RL [ssubst,iffD2]) 1);
    6.85  by (REPEAT (etac bexE 1
    6.86       ORELSE ares_tac ([bexI,iffI] @ (prems RL [iffD1,iffD2])) 1));
    6.87 -val bex_cong = result();
    6.88 +qed "bex_cong";
    6.89  
    6.90  (*** Rules for subsets ***)
    6.91  
    6.92  val prems = goalw Set.thy [subset_def] "(!!x.x:A ==> x:B) ==> A <= B";
    6.93  by (REPEAT (ares_tac (prems @ [ballI]) 1));
    6.94 -val subsetI = result();
    6.95 +qed "subsetI";
    6.96  
    6.97  (*Rule in Modus Ponens style*)
    6.98  val major::prems = goalw Set.thy [subset_def] "[| A <= B;  c:A |] ==> c:B";
    6.99  by (rtac (major RS bspec) 1);
   6.100  by (resolve_tac prems 1);
   6.101 -val subsetD = result();
   6.102 +qed "subsetD";
   6.103  
   6.104  (*Classical elimination rule*)
   6.105  val major::prems = goalw Set.thy [subset_def] 
   6.106      "[| A <= B;  ~(c:A) ==> P;  c:B ==> P |] ==> P";
   6.107  by (rtac (major RS ballE) 1);
   6.108  by (REPEAT (eresolve_tac prems 1));
   6.109 -val subsetCE = result();
   6.110 +qed "subsetCE";
   6.111  
   6.112  (*Takes assumptions A<=B; c:A and creates the assumption c:B *)
   6.113  fun set_mp_tac i = etac subsetCE i  THEN  mp_tac i;
   6.114  
   6.115 -val subset_refl = prove_goal Set.thy "A <= A"
   6.116 +qed_goal "subset_refl" Set.thy "A <= A"
   6.117   (fn _=> [ (REPEAT (ares_tac [subsetI] 1)) ]);
   6.118  
   6.119  goal Set.thy "!!A B C. [| A<=B;  B<=C |] ==> A<=C";
   6.120  by (rtac subsetI 1);
   6.121  by (REPEAT (eresolve_tac [asm_rl, subsetD] 1));
   6.122 -val subset_trans = result();
   6.123 +qed "subset_trans";
   6.124  
   6.125  
   6.126  (*** Rules for equality ***)
   6.127 @@ -128,31 +128,31 @@
   6.128  val prems = goal Set.thy "[| A <= B;  B <= A |] ==> A = B";
   6.129  by (rtac (iffI RS set_ext) 1);
   6.130  by (REPEAT (ares_tac (prems RL [subsetD]) 1));
   6.131 -val subset_antisym = result();
   6.132 +qed "subset_antisym";
   6.133  val equalityI = subset_antisym;
   6.134  
   6.135  (* Equality rules from ZF set theory -- are they appropriate here? *)
   6.136  val prems = goal Set.thy "A = B ==> A<=B";
   6.137  by (resolve_tac (prems RL [subst]) 1);
   6.138  by (rtac subset_refl 1);
   6.139 -val equalityD1 = result();
   6.140 +qed "equalityD1";
   6.141  
   6.142  val prems = goal Set.thy "A = B ==> B<=A";
   6.143  by (resolve_tac (prems RL [subst]) 1);
   6.144  by (rtac subset_refl 1);
   6.145 -val equalityD2 = result();
   6.146 +qed "equalityD2";
   6.147  
   6.148  val prems = goal Set.thy
   6.149      "[| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P";
   6.150  by (resolve_tac prems 1);
   6.151  by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1));
   6.152 -val equalityE = result();
   6.153 +qed "equalityE";
   6.154  
   6.155  val major::prems = goal Set.thy
   6.156      "[| A = B;  [| c:A; c:B |] ==> P;  [| ~ c:A; ~ c:B |] ==> P |]  ==>  P";
   6.157  by (rtac (major RS equalityE) 1);
   6.158  by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1));
   6.159 -val equalityCE = result();
   6.160 +qed "equalityCE";
   6.161  
   6.162  (*Lemma for creating induction formulae -- for "pattern matching" on p
   6.163    To make the induction hypotheses usable, apply "spec" or "bspec" to
   6.164 @@ -161,24 +161,24 @@
   6.165      "[| p:A;  !!z. z:A ==> p=z --> R |] ==> R";
   6.166  by (rtac mp 1);
   6.167  by (REPEAT (resolve_tac (refl::prems) 1));
   6.168 -val setup_induction = result();
   6.169 +qed "setup_induction";
   6.170  
   6.171  goal Set.thy "{x.x:A} = A";
   6.172  by (REPEAT (ares_tac [equalityI,subsetI,CollectI] 1  ORELSE etac CollectD 1));
   6.173 -val trivial_set = result();
   6.174 +qed "trivial_set";
   6.175  
   6.176  (*** Rules for binary union -- Un ***)
   6.177  
   6.178  val prems = goalw Set.thy [Un_def] "c:A ==> c : A Un B";
   6.179  by (REPEAT (resolve_tac (prems @ [CollectI,disjI1]) 1));
   6.180 -val UnI1 = result();
   6.181 +qed "UnI1";
   6.182  
   6.183  val prems = goalw Set.thy [Un_def] "c:B ==> c : A Un B";
   6.184  by (REPEAT (resolve_tac (prems @ [CollectI,disjI2]) 1));
   6.185 -val UnI2 = result();
   6.186 +qed "UnI2";
   6.187  
   6.188  (*Classical introduction rule: no commitment to A vs B*)
   6.189 -val UnCI = prove_goal Set.thy "(~c:B ==> c:A) ==> c : A Un B"
   6.190 +qed_goal "UnCI" Set.thy "(~c:B ==> c:A) ==> c : A Un B"
   6.191   (fn prems=>
   6.192    [ (rtac classical 1),
   6.193      (REPEAT (ares_tac (prems@[UnI1,notI]) 1)),
   6.194 @@ -188,7 +188,7 @@
   6.195      "[| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P";
   6.196  by (rtac (major RS CollectD RS disjE) 1);
   6.197  by (REPEAT (eresolve_tac prems 1));
   6.198 -val UnE = result();
   6.199 +qed "UnE";
   6.200  
   6.201  
   6.202  (*** Rules for small intersection -- Int ***)
   6.203 @@ -196,22 +196,22 @@
   6.204  val prems = goalw Set.thy [Int_def]
   6.205      "[| c:A;  c:B |] ==> c : A Int B";
   6.206  by (REPEAT (resolve_tac (prems @ [CollectI,conjI]) 1));
   6.207 -val IntI = result();
   6.208 +qed "IntI";
   6.209  
   6.210  val [major] = goalw Set.thy [Int_def] "c : A Int B ==> c:A";
   6.211  by (rtac (major RS CollectD RS conjunct1) 1);
   6.212 -val IntD1 = result();
   6.213 +qed "IntD1";
   6.214  
   6.215  val [major] = goalw Set.thy [Int_def] "c : A Int B ==> c:B";
   6.216  by (rtac (major RS CollectD RS conjunct2) 1);
   6.217 -val IntD2 = result();
   6.218 +qed "IntD2";
   6.219  
   6.220  val [major,minor] = goal Set.thy
   6.221      "[| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P";
   6.222  by (rtac minor 1);
   6.223  by (rtac (major RS IntD1) 1);
   6.224  by (rtac (major RS IntD2) 1);
   6.225 -val IntE = result();
   6.226 +qed "IntE";
   6.227  
   6.228  
   6.229  (*** Rules for set complement -- Compl ***)
   6.230 @@ -219,7 +219,7 @@
   6.231  val prems = goalw Set.thy [Compl_def]
   6.232      "[| c:A ==> False |] ==> c : Compl(A)";
   6.233  by (REPEAT (ares_tac (prems @ [CollectI,notI]) 1));
   6.234 -val ComplI = result();
   6.235 +qed "ComplI";
   6.236  
   6.237  (*This form, with negated conclusion, works well with the Classical prover.
   6.238    Negated assumptions behave like formulae on the right side of the notional
   6.239 @@ -227,7 +227,7 @@
   6.240  val major::prems = goalw Set.thy [Compl_def]
   6.241      "[| c : Compl(A) |] ==> ~c:A";
   6.242  by (rtac (major RS CollectD) 1);
   6.243 -val ComplD = result();
   6.244 +qed "ComplD";
   6.245  
   6.246  val ComplE = make_elim ComplD;
   6.247  
   6.248 @@ -236,11 +236,11 @@
   6.249  
   6.250  goalw Set.thy [empty_def] "{x.False} = {}";
   6.251  by (rtac refl 1);
   6.252 -val empty_eq = result();
   6.253 +qed "empty_eq";
   6.254  
   6.255  val [prem] = goalw Set.thy [empty_def] "a : {} ==> P";
   6.256  by (rtac (prem RS CollectD RS FalseE) 1);
   6.257 -val emptyD = result();
   6.258 +qed "emptyD";
   6.259  
   6.260  val emptyE = make_elim emptyD;
   6.261  
   6.262 @@ -248,18 +248,18 @@
   6.263  by (rtac (prem RS swap) 1);
   6.264  by (rtac equalityI 1);
   6.265  by (ALLGOALS (fast_tac (FOL_cs addSIs [subsetI] addSEs [emptyD])));
   6.266 -val not_emptyD = result();
   6.267 +qed "not_emptyD";
   6.268  
   6.269  (*** Singleton sets ***)
   6.270  
   6.271  goalw Set.thy [singleton_def] "a : {a}";
   6.272  by (rtac CollectI 1);
   6.273  by (rtac refl 1);
   6.274 -val singletonI = result();
   6.275 +qed "singletonI";
   6.276  
   6.277  val [major] = goalw Set.thy [singleton_def] "b : {a} ==> b=a"; 
   6.278  by (rtac (major RS CollectD) 1);
   6.279 -val singletonD = result();
   6.280 +qed "singletonD";
   6.281  
   6.282  val singletonE = make_elim singletonD;
   6.283  
   6.284 @@ -269,13 +269,13 @@
   6.285  val prems = goalw Set.thy [UNION_def]
   6.286      "[| a:A;  b: B(a) |] ==> b: (UN x:A. B(x))";
   6.287  by (REPEAT (resolve_tac (prems @ [bexI,CollectI]) 1));
   6.288 -val UN_I = result();
   6.289 +qed "UN_I";
   6.290  
   6.291  val major::prems = goalw Set.thy [UNION_def]
   6.292      "[| b : (UN x:A. B(x));  !!x.[| x:A;  b: B(x) |] ==> R |] ==> R";
   6.293  by (rtac (major RS CollectD RS bexE) 1);
   6.294  by (REPEAT (ares_tac prems 1));
   6.295 -val UN_E = result();
   6.296 +qed "UN_E";
   6.297  
   6.298  val prems = goal Set.thy
   6.299      "[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==> \
   6.300 @@ -283,27 +283,27 @@
   6.301  by (REPEAT (etac UN_E 1
   6.302       ORELSE ares_tac ([UN_I,equalityI,subsetI] @ 
   6.303  		      (prems RL [equalityD1,equalityD2] RL [subsetD])) 1));
   6.304 -val UN_cong = result();
   6.305 +qed "UN_cong";
   6.306  
   6.307  (*** Intersections of families -- INTER x:A. B(x) is Inter(B)``A ) *)
   6.308  
   6.309  val prems = goalw Set.thy [INTER_def]
   6.310      "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))";
   6.311  by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1));
   6.312 -val INT_I = result();
   6.313 +qed "INT_I";
   6.314  
   6.315  val major::prems = goalw Set.thy [INTER_def]
   6.316      "[| b : (INT x:A. B(x));  a:A |] ==> b: B(a)";
   6.317  by (rtac (major RS CollectD RS bspec) 1);
   6.318  by (resolve_tac prems 1);
   6.319 -val INT_D = result();
   6.320 +qed "INT_D";
   6.321  
   6.322  (*"Classical" elimination rule -- does not require proving X:C *)
   6.323  val major::prems = goalw Set.thy [INTER_def]
   6.324      "[| b : (INT x:A. B(x));  b: B(a) ==> R;  ~ a:A ==> R |] ==> R";
   6.325  by (rtac (major RS CollectD RS ballE) 1);
   6.326  by (REPEAT (eresolve_tac prems 1));
   6.327 -val INT_E = result();
   6.328 +qed "INT_E";
   6.329  
   6.330  val prems = goal Set.thy
   6.331      "[| A=B;  !!x. x:B ==> C(x) = D(x) |] ==> \
   6.332 @@ -311,7 +311,7 @@
   6.333  by (REPEAT_FIRST (resolve_tac [INT_I,equalityI,subsetI]));
   6.334  by (REPEAT (dtac INT_D 1
   6.335       ORELSE ares_tac (prems RL [equalityD1,equalityD2] RL [subsetD]) 1));
   6.336 -val INT_cong = result();
   6.337 +qed "INT_cong";
   6.338  
   6.339  (*** Rules for Unions ***)
   6.340  
   6.341 @@ -319,20 +319,20 @@
   6.342  val prems = goalw Set.thy [Union_def]
   6.343      "[| X:C;  A:X |] ==> A : Union(C)";
   6.344  by (REPEAT (resolve_tac (prems @ [UN_I]) 1));
   6.345 -val UnionI = result();
   6.346 +qed "UnionI";
   6.347  
   6.348  val major::prems = goalw Set.thy [Union_def]
   6.349      "[| A : Union(C);  !!X.[| A:X;  X:C |] ==> R |] ==> R";
   6.350  by (rtac (major RS UN_E) 1);
   6.351  by (REPEAT (ares_tac prems 1));
   6.352 -val UnionE = result();
   6.353 +qed "UnionE";
   6.354  
   6.355  (*** Rules for Inter ***)
   6.356  
   6.357  val prems = goalw Set.thy [Inter_def]
   6.358      "[| !!X. X:C ==> A:X |] ==> A : Inter(C)";
   6.359  by (REPEAT (ares_tac ([INT_I] @ prems) 1));
   6.360 -val InterI = result();
   6.361 +qed "InterI";
   6.362  
   6.363  (*A "destruct" rule -- every X in C contains A as an element, but
   6.364    A:X can hold when X:C does not!  This rule is analogous to "spec". *)
   6.365 @@ -340,11 +340,11 @@
   6.366      "[| A : Inter(C);  X:C |] ==> A:X";
   6.367  by (rtac (major RS INT_D) 1);
   6.368  by (resolve_tac prems 1);
   6.369 -val InterD = result();
   6.370 +qed "InterD";
   6.371  
   6.372  (*"Classical" elimination rule -- does not require proving X:C *)
   6.373  val major::prems = goalw Set.thy [Inter_def]
   6.374      "[| A : Inter(C);  A:X ==> R;  ~ X:C ==> R |] ==> R";
   6.375  by (rtac (major RS INT_E) 1);
   6.376  by (REPEAT (eresolve_tac prems 1));
   6.377 -val InterE = result();
   6.378 +qed "InterE";
     7.1 --- a/src/CCL/Term.ML	Wed Nov 30 13:18:42 1994 +0100
     7.2 +++ b/src/CCL/Term.ML	Wed Nov 30 13:53:46 1994 +0100
     7.3 @@ -24,34 +24,34 @@
     7.4  goalw Term.thy [let_def] "~ t=bot--> let x be t in f(x) = f(t)";
     7.5  by (res_inst_tac [("t","t")] term_case 1);
     7.6  by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
     7.7 -val letB = result() RS mp;
     7.8 +val letB = store_thm("letB", result() RS mp);
     7.9  
    7.10  goalw Term.thy [let_def] "let x be bot in f(x) = bot";
    7.11  by (rtac caseBbot 1);
    7.12 -val letBabot = result();
    7.13 +qed "letBabot";
    7.14  
    7.15  goalw Term.thy [let_def] "let x be t in bot = bot";
    7.16  by (resolve_tac ([caseBbot] RL [term_case]) 1);
    7.17  by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
    7.18 -val letBbbot = result();
    7.19 +qed "letBbbot";
    7.20  
    7.21  goalw Term.thy [apply_def] "(lam x.b(x)) ` a = b(a)";
    7.22  by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
    7.23 -val applyB = result();
    7.24 +qed "applyB";
    7.25  
    7.26  goalw Term.thy [apply_def] "bot ` a = bot";
    7.27  by (rtac caseBbot 1);
    7.28 -val applyBbot = result();
    7.29 +qed "applyBbot";
    7.30  
    7.31  goalw Term.thy [fix_def] "fix(f) = f(fix(f))";
    7.32  by (resolve_tac [applyB RS ssubst] 1 THEN rtac refl 1);
    7.33 -val fixB = result();
    7.34 +qed "fixB";
    7.35  
    7.36  goalw Term.thy [letrec_def]
    7.37        "letrec g x be h(x,g) in g(a) = h(a,%y.letrec g x be h(x,g) in g(y))";
    7.38  by (resolve_tac [fixB RS ssubst] 1 THEN 
    7.39      resolve_tac [applyB RS ssubst] 1 THEN rtac refl 1);
    7.40 -val letrecB = result();
    7.41 +qed "letrecB";
    7.42  
    7.43  val rawBs = caseBs @ [applyB,applyBbot];
    7.44  
     8.1 --- a/src/CCL/Trancl.ML	Wed Nov 30 13:18:42 1994 +0100
     8.2 +++ b/src/CCL/Trancl.ML	Wed Nov 30 13:53:46 1994 +0100
     8.3 @@ -17,13 +17,13 @@
     8.4  val prems = goalw Trancl.thy [trans_def]
     8.5      "(!! x y z. [| <x,y>:r;  <y,z>:r |] ==> <x,z>:r) ==> trans(r)";
     8.6  by (REPEAT (ares_tac (prems@[allI,impI]) 1));
     8.7 -val transI = result();
     8.8 +qed "transI";
     8.9  
    8.10  val major::prems = goalw Trancl.thy [trans_def]
    8.11      "[| trans(r);  <a,b>:r;  <b,c>:r |] ==> <a,c>:r";
    8.12  by (cut_facts_tac [major] 1);
    8.13  by (fast_tac (FOL_cs addIs prems) 1);
    8.14 -val transD = result();
    8.15 +qed "transD";
    8.16  
    8.17  (** Identity relation **)
    8.18  
    8.19 @@ -31,7 +31,7 @@
    8.20  by (rtac CollectI 1);
    8.21  by (rtac exI 1);
    8.22  by (rtac refl 1);
    8.23 -val idI = result();
    8.24 +qed "idI";
    8.25  
    8.26  val major::prems = goalw Trancl.thy [id_def]
    8.27      "[| p: id;  !!x.[| p = <x,x> |] ==> P  \
    8.28 @@ -39,14 +39,14 @@
    8.29  by (rtac (major RS CollectE) 1);
    8.30  by (etac exE 1);
    8.31  by (eresolve_tac prems 1);
    8.32 -val idE = result();
    8.33 +qed "idE";
    8.34  
    8.35  (** Composition of two relations **)
    8.36  
    8.37  val prems = goalw Trancl.thy [comp_def]
    8.38      "[| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s";
    8.39  by (fast_tac (set_cs addIs prems) 1);
    8.40 -val compI = result();
    8.41 +qed "compI";
    8.42  
    8.43  (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
    8.44  val prems = goalw Trancl.thy [comp_def]
    8.45 @@ -55,7 +55,7 @@
    8.46  \    |] ==> P";
    8.47  by (cut_facts_tac prems 1);
    8.48  by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1));
    8.49 -val compE = result();
    8.50 +qed "compE";
    8.51  
    8.52  val prems = goal Trancl.thy
    8.53      "[| <a,c> : r O s;  \
    8.54 @@ -63,7 +63,7 @@
    8.55  \    |] ==> P";
    8.56  by (rtac compE 1);
    8.57  by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [pair_inject,ssubst] 1));
    8.58 -val compEpair = result();
    8.59 +qed "compEpair";
    8.60  
    8.61  val comp_cs = set_cs addIs [compI,idI] 
    8.62  		       addEs [compE,idE] 
    8.63 @@ -73,14 +73,14 @@
    8.64      "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
    8.65  by (cut_facts_tac prems 1);
    8.66  by (fast_tac comp_cs 1);
    8.67 -val comp_mono = result();
    8.68 +qed "comp_mono";
    8.69  
    8.70  (** The relation rtrancl **)
    8.71  
    8.72  goal Trancl.thy "mono(%s. id Un (r O s))";
    8.73  by (rtac monoI 1);
    8.74  by (REPEAT (ares_tac [monoI, subset_refl, comp_mono, Un_mono] 1));
    8.75 -val rtrancl_fun_mono = result();
    8.76 +qed "rtrancl_fun_mono";
    8.77  
    8.78  val rtrancl_unfold = rtrancl_fun_mono RS (rtrancl_def RS def_lfp_Tarski);
    8.79  
    8.80 @@ -88,20 +88,20 @@
    8.81  goal Trancl.thy "<a,a> : r^*";
    8.82  by (rtac (rtrancl_unfold RS ssubst) 1);
    8.83  by (fast_tac comp_cs 1);
    8.84 -val rtrancl_refl = result();
    8.85 +qed "rtrancl_refl";
    8.86  
    8.87  (*Closure under composition with r*)
    8.88  val prems = goal Trancl.thy
    8.89      "[| <a,b> : r^*;  <b,c> : r |] ==> <a,c> : r^*";
    8.90  by (rtac (rtrancl_unfold RS ssubst) 1);
    8.91  by (fast_tac (comp_cs addIs prems) 1);
    8.92 -val rtrancl_into_rtrancl = result();
    8.93 +qed "rtrancl_into_rtrancl";
    8.94  
    8.95  (*rtrancl of r contains r*)
    8.96  val [prem] = goal Trancl.thy "[| <a,b> : r |] ==> <a,b> : r^*";
    8.97  by (rtac (rtrancl_refl RS rtrancl_into_rtrancl) 1);
    8.98  by (rtac prem 1);
    8.99 -val r_into_rtrancl = result();
   8.100 +qed "r_into_rtrancl";
   8.101  
   8.102  
   8.103  (** standard induction rule **)
   8.104 @@ -114,7 +114,7 @@
   8.105  by (rtac (major RS (rtrancl_def RS def_induct)) 1);
   8.106  by (rtac rtrancl_fun_mono 1);
   8.107  by (fast_tac (comp_cs addIs prems) 1);
   8.108 -val rtrancl_full_induct = result();
   8.109 +qed "rtrancl_full_induct";
   8.110  
   8.111  (*nice induction rule*)
   8.112  val major::prems = goal Trancl.thy
   8.113 @@ -130,14 +130,14 @@
   8.114  by (resolve_tac [major RS rtrancl_full_induct] 1);
   8.115  by (fast_tac (comp_cs addIs prems) 1);
   8.116  by (fast_tac (comp_cs addIs prems) 1);
   8.117 -val rtrancl_induct = result();
   8.118 +qed "rtrancl_induct";
   8.119  
   8.120  (*transitivity of transitive closure!! -- by induction.*)
   8.121  goal Trancl.thy "trans(r^*)";
   8.122  by (rtac transI 1);
   8.123  by (res_inst_tac [("b","z")] rtrancl_induct 1);
   8.124  by (DEPTH_SOLVE (eresolve_tac [asm_rl, rtrancl_into_rtrancl] 1));
   8.125 -val trans_rtrancl = result();
   8.126 +qed "trans_rtrancl";
   8.127  
   8.128  (*elimination of rtrancl -- by induction on a special formula*)
   8.129  val major::prems = goal Trancl.thy
   8.130 @@ -149,7 +149,7 @@
   8.131  by (fast_tac (set_cs addIs prems) 2);
   8.132  by (fast_tac (set_cs addIs prems) 2);
   8.133  by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
   8.134 -val rtranclE = result();
   8.135 +qed "rtranclE";
   8.136  
   8.137  
   8.138  (**** The relation trancl ****)
   8.139 @@ -160,19 +160,19 @@
   8.140      "[| <a,b> : r^+ |] ==> <a,b> : r^*";
   8.141  by (resolve_tac [major RS compEpair] 1);
   8.142  by (REPEAT (ares_tac [rtrancl_into_rtrancl] 1));
   8.143 -val trancl_into_rtrancl = result();
   8.144 +qed "trancl_into_rtrancl";
   8.145  
   8.146  (*r^+ contains r*)
   8.147  val [prem] = goalw Trancl.thy [trancl_def]
   8.148     "[| <a,b> : r |] ==> <a,b> : r^+";
   8.149  by (REPEAT (ares_tac [prem,compI,rtrancl_refl] 1));
   8.150 -val r_into_trancl = result();
   8.151 +qed "r_into_trancl";
   8.152  
   8.153  (*intro rule by definition: from rtrancl and r*)
   8.154  val prems = goalw Trancl.thy [trancl_def]
   8.155      "[| <a,b> : r^*;  <b,c> : r |]   ==>  <a,c> : r^+";
   8.156  by (REPEAT (resolve_tac ([compI]@prems) 1));
   8.157 -val rtrancl_into_trancl1 = result();
   8.158 +qed "rtrancl_into_trancl1";
   8.159  
   8.160  (*intro rule from r and rtrancl*)
   8.161  val prems = goal Trancl.thy
   8.162 @@ -182,7 +182,7 @@
   8.163  by (resolve_tac (prems RL [r_into_trancl]) 1);
   8.164  by (rtac (trans_rtrancl RS transD RS rtrancl_into_trancl1) 1);
   8.165  by (REPEAT (ares_tac (prems@[r_into_rtrancl]) 1));
   8.166 -val rtrancl_into_trancl2 = result();
   8.167 +qed "rtrancl_into_trancl2";
   8.168  
   8.169  (*elimination of r^+ -- NOT an induction rule*)
   8.170  val major::prems = goal Trancl.thy
   8.171 @@ -196,7 +196,7 @@
   8.172  by (etac rtranclE 1);
   8.173  by (fast_tac comp_cs 1);
   8.174  by (fast_tac (comp_cs addSIs [rtrancl_into_trancl1]) 1);
   8.175 -val tranclE = result();
   8.176 +qed "tranclE";
   8.177  
   8.178  (*Transitivity of r^+.
   8.179    Proved by unfolding since it uses transitivity of rtrancl. *)
   8.180 @@ -205,11 +205,11 @@
   8.181  by (REPEAT (etac compEpair 1));
   8.182  by (rtac (rtrancl_into_rtrancl RS (trans_rtrancl RS transD RS compI)) 1);
   8.183  by (REPEAT (assume_tac 1));
   8.184 -val trans_trancl = result();
   8.185 +qed "trans_trancl";
   8.186  
   8.187  val prems = goal Trancl.thy
   8.188      "[| <a,b> : r;  <b,c> : r^+ |]   ==>  <a,c> : r^+";
   8.189  by (rtac (r_into_trancl RS (trans_trancl RS transD)) 1);
   8.190  by (resolve_tac prems 1);
   8.191  by (resolve_tac prems 1);
   8.192 -val trancl_into_trancl2 = result();
   8.193 +qed "trancl_into_trancl2";
     9.1 --- a/src/CCL/Type.ML	Wed Nov 30 13:18:42 1994 +0100
     9.2 +++ b/src/CCL/Type.ML	Wed Nov 30 13:53:46 1994 +0100
     9.3 @@ -17,7 +17,7 @@
     9.4  
     9.5  goal Set.thy "A <= B <-> (ALL x.x:A --> x:B)";
     9.6  by (fast_tac set_cs 1);
     9.7 -val subsetXH = result();
     9.8 +qed "subsetXH";
     9.9  
    9.10  (*** Exhaustion Rules ***)
    9.11  
    9.12 @@ -99,22 +99,22 @@
    9.13  val prems = goal Type.thy
    9.14       "[| a:A;  P(a) |] ==> a : {x:A. P(x)}";
    9.15  by (REPEAT (resolve_tac (prems@[SubtypeXH RS iffD2,conjI]) 1));
    9.16 -val SubtypeI = result();
    9.17 +qed "SubtypeI";
    9.18  
    9.19  val prems = goal Type.thy
    9.20       "[| a : {x:A. P(x)};  [| a:A;  P(a) |] ==> Q |] ==> Q";
    9.21  by (REPEAT (resolve_tac (prems@[SubtypeD1,SubtypeD2]) 1));
    9.22 -val SubtypeE = result();
    9.23 +qed "SubtypeE";
    9.24  
    9.25  (*** Monotonicity ***)
    9.26  
    9.27  goal Type.thy "mono (%X.X)";
    9.28  by (REPEAT (ares_tac [monoI] 1));
    9.29 -val idM = result();
    9.30 +qed "idM";
    9.31  
    9.32  goal Type.thy "mono(%X.A)";
    9.33  by (REPEAT (ares_tac [monoI,subset_refl] 1));
    9.34 -val constM = result();
    9.35 +qed "constM";
    9.36  
    9.37  val major::prems = goal Type.thy
    9.38      "mono(%X.A(X)) ==> mono(%X.[A(X)])";
    9.39 @@ -125,7 +125,7 @@
    9.40  by (rtac (disjI2 RS (LiftXH RS iffD2)) 1);
    9.41  by (etac (major RS monoD RS subsetD) 1);
    9.42  by (assume_tac 1);
    9.43 -val LiftM = result();
    9.44 +qed "LiftM";
    9.45  
    9.46  val prems = goal Type.thy
    9.47      "[| mono(%X.A(X)); !!x X. x:A(X) ==> mono(%X.B(X,x)) |] ==> \
    9.48 @@ -134,7 +134,7 @@
    9.49              eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
    9.50              (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
    9.51              hyp_subst_tac 1));
    9.52 -val SgM = result();
    9.53 +qed "SgM";
    9.54  
    9.55  val prems = goal Type.thy
    9.56      "[| !!x. x:A ==> mono(%X.B(X,x)) |] ==> mono(%X.Pi(A,B(X)))";
    9.57 @@ -142,7 +142,7 @@
    9.58              eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
    9.59              (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
    9.60              hyp_subst_tac 1));
    9.61 -val PiM = result();
    9.62 +qed "PiM";
    9.63  
    9.64  val prems = goal Type.thy
    9.65       "[| mono(%X.A(X));  mono(%X.B(X)) |] ==> mono(%X.A(X)+B(X))";
    9.66 @@ -150,7 +150,7 @@
    9.67              eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
    9.68              (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
    9.69              hyp_subst_tac 1));
    9.70 -val PlusM = result();
    9.71 +qed "PlusM";
    9.72  
    9.73  (**************** RECURSIVE TYPES ******************)
    9.74  
    9.75 @@ -158,19 +158,19 @@
    9.76  
    9.77  goal Type.thy "mono(%X.Unit+X)";
    9.78  by (REPEAT (ares_tac [PlusM,constM,idM] 1));
    9.79 -val NatM = result();
    9.80 -val def_NatB = result() RS (Nat_def RS def_lfp_Tarski);
    9.81 +qed "NatM";
    9.82 +val def_NatB = store_thm("def_NatB", result() RS (Nat_def RS def_lfp_Tarski));
    9.83  
    9.84  goal Type.thy "mono(%X.(Unit+Sigma(A,%y.X)))";
    9.85  by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
    9.86 -val ListM = result();
    9.87 -val def_ListB = result() RS (List_def RS def_lfp_Tarski);
    9.88 -val def_ListsB = result() RS (Lists_def RS def_gfp_Tarski);
    9.89 +qed "ListM";
    9.90 +val def_ListB = store_thm("def_ListB", result() RS (List_def RS def_lfp_Tarski));
    9.91 +val def_ListsB = store_thm("def_ListsB", result() RS (Lists_def RS def_gfp_Tarski));
    9.92  
    9.93  goal Type.thy "mono(%X.({} + Sigma(A,%y.X)))";
    9.94  by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
    9.95 -val IListsM = result();
    9.96 -val def_IListsB = result() RS (ILists_def RS def_gfp_Tarski);
    9.97 +qed "IListsM";
    9.98 +val def_IListsB = store_thm("def_IListsB", result() RS (ILists_def RS def_gfp_Tarski));
    9.99  
   9.100  val ind_type_eqs = [def_NatB,def_ListB,def_ListsB,def_IListsB];
   9.101  
   9.102 @@ -264,7 +264,7 @@
   9.103  by (rtac (major RS (XH_to_E SgXH)) 1);
   9.104  by (rtac minor 1);
   9.105  by (ALLGOALS (fast_tac term_cs));
   9.106 -val SgE2 = result();
   9.107 +qed "SgE2";
   9.108  
   9.109  (* General theorem proving ignores non-canonical term-formers,             *)
   9.110  (*         - intro rules are type rules for canonical terms                *)
   9.111 @@ -280,7 +280,7 @@
   9.112  by (rtac (lfp_lowerbound RS subset_trans) 1);
   9.113  by (rtac (mono RS gfp_lemma3) 1);
   9.114  by (rtac subset_refl 1);
   9.115 -val lfp_subset_gfp = result();
   9.116 +qed "lfp_subset_gfp";
   9.117  
   9.118  val prems = goal Type.thy
   9.119      "[| a:A;  !!x X.[| x:A;  ALL y:A.t(y):X |] ==> t(x) : B(X) |] ==> \
   9.120 @@ -288,14 +288,14 @@
   9.121  by (rtac coinduct 1);
   9.122  by (res_inst_tac [("P","%x.EX y:A.x=t(y)")] CollectI 1);
   9.123  by (ALLGOALS (fast_tac (ccl_cs addSIs prems)));
   9.124 -val gfpI = result();
   9.125 +qed "gfpI";
   9.126  
   9.127  val rew::prem::prems = goal Type.thy
   9.128      "[| C==gfp(B);  a:A;  !!x X.[| x:A;  ALL y:A.t(y):X |] ==> t(x) : B(X) |] ==> \
   9.129  \    t(a) : C";
   9.130  by (rewtac rew);
   9.131  by (REPEAT (ares_tac ((prem RS gfpI)::prems) 1));
   9.132 -val def_gfpI = result();
   9.133 +qed "def_gfpI";
   9.134  
   9.135  (* EG *)
   9.136  
    10.1 --- a/src/CCL/Wfd.ML	Wed Nov 30 13:18:42 1994 +0100
    10.2 +++ b/src/CCL/Wfd.ML	Wed Nov 30 13:53:46 1994 +0100
    10.3 @@ -20,7 +20,7 @@
    10.4  \    P(a)";
    10.5  by (rtac (major RS spec RS mp RS spec RS CollectD) 1);
    10.6  by (fast_tac (set_cs addSIs [prem RS CollectI]) 1);
    10.7 -val wfd_induct = result();
    10.8 +qed "wfd_induct";
    10.9  
   10.10  val [p1,p2,p3] = goal Wfd.thy
   10.11      "[| !!x y.<x,y> : R ==> Q(x); \
   10.12 @@ -28,7 +28,7 @@
   10.13  \       !!x.Q(x) ==> x:P |] ==> a:P";
   10.14  by (rtac (p2 RS  spec  RS mp) 1);
   10.15  by (fast_tac (set_cs addSIs [p1 RS p3]) 1);
   10.16 -val wfd_strengthen_lemma = result();
   10.17 +qed "wfd_strengthen_lemma";
   10.18  
   10.19  fun wfd_strengthen_tac s i = res_inst_tac [("Q",s)] wfd_strengthen_lemma i THEN
   10.20                               assume_tac (i+1);
   10.21 @@ -38,12 +38,12 @@
   10.22  by (fast_tac (FOL_cs addIs prems) 1);
   10.23  by (rtac (wfd RS  wfd_induct) 1);
   10.24  by (ALLGOALS (fast_tac (ccl_cs addSIs prems)));
   10.25 -val wf_anti_sym = result();
   10.26 +qed "wf_anti_sym";
   10.27  
   10.28  val prems = goal Wfd.thy "[| Wfd(r);  <a,a>: r |] ==> P";
   10.29  by (rtac wf_anti_sym 1);
   10.30  by (REPEAT (resolve_tac prems 1));
   10.31 -val wf_anti_refl = result();
   10.32 +qed "wf_anti_refl";
   10.33  
   10.34  (*** Irreflexive transitive closure ***)
   10.35  
   10.36 @@ -59,24 +59,24 @@
   10.37  by (fast_tac ccl_cs 1);
   10.38  by (etac (spec RS mp RS spec RS mp) 1);
   10.39  by (REPEAT (atac 1));
   10.40 -val trancl_wf = result();
   10.41 +qed "trancl_wf";
   10.42  
   10.43  (*** Lexicographic Ordering ***)
   10.44  
   10.45  goalw Wfd.thy [lex_def] 
   10.46   "p : ra**rb <-> (EX a a' b b'.p = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb))";
   10.47  by (fast_tac ccl_cs 1);
   10.48 -val lexXH = result();
   10.49 +qed "lexXH";
   10.50  
   10.51  val prems = goal Wfd.thy
   10.52   "<a,a'> : ra ==> <<a,b>,<a',b'>> : ra**rb";
   10.53  by (fast_tac (ccl_cs addSIs (prems @ [lexXH RS iffD2])) 1);
   10.54 -val lexI1 = result();
   10.55 +qed "lexI1";
   10.56  
   10.57  val prems = goal Wfd.thy
   10.58   "<b,b'> : rb ==> <<a,b>,<a,b'>> : ra**rb";
   10.59  by (fast_tac (ccl_cs addSIs (prems @ [lexXH RS iffD2])) 1);
   10.60 -val lexI2 = result();
   10.61 +qed "lexI2";
   10.62  
   10.63  val major::prems = goal Wfd.thy
   10.64   "[| p : ra**rb;  \
   10.65 @@ -86,13 +86,13 @@
   10.66  by (rtac (major RS (lexXH RS iffD1) RS exE) 1);
   10.67  by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems)));
   10.68  by (ALLGOALS (fast_tac ccl_cs));
   10.69 -val lexE = result();
   10.70 +qed "lexE";
   10.71  
   10.72  val [major,minor] = goal Wfd.thy
   10.73   "[| p : r**s;  !!a a' b b'. p = <<a,b>,<a',b'>> ==> P |] ==>P";
   10.74  by (rtac (major RS lexE) 1);
   10.75  by (ALLGOALS (fast_tac (set_cs addSEs [minor])));
   10.76 -val lex_pair = result();
   10.77 +qed "lex_pair";
   10.78  
   10.79  val [wfa,wfb] = goal Wfd.thy
   10.80   "[| Wfd(R); Wfd(S) |] ==> Wfd(R**S)";
   10.81 @@ -105,26 +105,26 @@
   10.82  by (rtac (wfa RS wfd_induct RS allI) 1);
   10.83  by (rtac (wfb RS wfd_induct RS allI) 1);back();
   10.84  by (fast_tac (type_cs addSEs [lexE]) 1);
   10.85 -val lex_wf = result();
   10.86 +qed "lex_wf";
   10.87  
   10.88  (*** Mapping ***)
   10.89  
   10.90  goalw Wfd.thy [wmap_def] 
   10.91   "p : wmap(f,r) <-> (EX x y. p=<x,y>  &  <f(x),f(y)> : r)";
   10.92  by (fast_tac ccl_cs 1);
   10.93 -val wmapXH = result();
   10.94 +qed "wmapXH";
   10.95  
   10.96  val prems = goal Wfd.thy
   10.97   "<f(a),f(b)> : r ==> <a,b> : wmap(f,r)";
   10.98  by (fast_tac (ccl_cs addSIs (prems @ [wmapXH RS iffD2])) 1);
   10.99 -val wmapI = result();
  10.100 +qed "wmapI";
  10.101  
  10.102  val major::prems = goal Wfd.thy
  10.103   "[| p : wmap(f,r);  !!a b.[| <f(a),f(b)> : r;  p=<a,b> |] ==> R |] ==> R";
  10.104  by (rtac (major RS (wmapXH RS iffD1) RS exE) 1);
  10.105  by (REPEAT_SOME (eresolve_tac ([exE,conjE,disjE]@prems)));
  10.106  by (ALLGOALS (fast_tac ccl_cs));
  10.107 -val wmapE = result();
  10.108 +qed "wmapE";
  10.109  
  10.110  val [wf] = goal Wfd.thy
  10.111   "Wfd(r) ==> Wfd(wmap(f,r))";
  10.112 @@ -139,49 +139,49 @@
  10.113  by (etac (spec RS mp RS spec RS mp) 1);
  10.114  by (assume_tac 1);
  10.115  by (rtac refl 1);
  10.116 -val wmap_wf = result();
  10.117 +qed "wmap_wf";
  10.118  
  10.119  (* Projections *)
  10.120  
  10.121  val prems = goal Wfd.thy "<xa,ya> : r ==> <<xa,xb>,<ya,yb>> : wmap(fst,r)";
  10.122  by (rtac wmapI 1);
  10.123  by (simp_tac (term_ss addsimps prems) 1);
  10.124 -val wfstI = result();
  10.125 +qed "wfstI";
  10.126  
  10.127  val prems = goal Wfd.thy "<xb,yb> : r ==> <<xa,xb>,<ya,yb>> : wmap(snd,r)";
  10.128  by (rtac wmapI 1);
  10.129  by (simp_tac (term_ss addsimps prems) 1);
  10.130 -val wsndI = result();
  10.131 +qed "wsndI";
  10.132  
  10.133  val prems = goal Wfd.thy "<xc,yc> : r ==> <<xa,<xb,xc>>,<ya,<yb,yc>>> : wmap(thd,r)";
  10.134  by (rtac wmapI 1);
  10.135  by (simp_tac (term_ss addsimps prems) 1);
  10.136 -val wthdI = result();
  10.137 +qed "wthdI";
  10.138  
  10.139  (*** Ground well-founded relations ***)
  10.140  
  10.141  val prems = goalw Wfd.thy [wf_def] 
  10.142      "[| Wfd(r);  a : r |] ==> a : wf(r)";
  10.143  by (fast_tac (set_cs addSIs prems) 1);
  10.144 -val wfI = result();
  10.145 +qed "wfI";
  10.146  
  10.147  val prems = goalw Wfd.thy [Wfd_def] "Wfd({})";
  10.148  by (fast_tac (set_cs addEs [EmptyXH RS iffD1 RS FalseE]) 1);
  10.149 -val Empty_wf = result();
  10.150 +qed "Empty_wf";
  10.151  
  10.152  val prems = goalw Wfd.thy [wf_def] "Wfd(wf(R))";
  10.153  by (res_inst_tac [("Q","Wfd(R)")] (excluded_middle RS disjE) 1);
  10.154  by (ALLGOALS (asm_simp_tac CCL_ss));
  10.155  by (rtac Empty_wf 1);
  10.156 -val wf_wf = result();
  10.157 +qed "wf_wf";
  10.158  
  10.159  goalw Wfd.thy [NatPR_def]  "p : NatPR <-> (EX x:Nat.p=<x,succ(x)>)";
  10.160  by (fast_tac set_cs 1);
  10.161 -val NatPRXH = result();
  10.162 +qed "NatPRXH";
  10.163  
  10.164  goalw Wfd.thy [ListPR_def]  "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h$t>)";
  10.165  by (fast_tac set_cs 1);
  10.166 -val ListPRXH = result();
  10.167 +qed "ListPRXH";
  10.168  
  10.169  val NatPRI = refl RS (bexI RS (NatPRXH RS iffD2));
  10.170  val ListPRI = refl RS (bexI RS (bexI RS (ListPRXH RS iffD2)));
  10.171 @@ -192,7 +192,7 @@
  10.172  by (fast_tac (type_cs addSEs [XH_to_E NatPRXH]) 1);
  10.173  by (etac Nat_ind 1);
  10.174  by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E NatPRXH])));
  10.175 -val NatPR_wf = result();
  10.176 +qed "NatPR_wf";
  10.177  
  10.178  goalw Wfd.thy [Wfd_def]  "Wfd(ListPR(A))";
  10.179  by (safe_tac set_cs);
  10.180 @@ -200,5 +200,5 @@
  10.181  by (fast_tac (type_cs addSEs [XH_to_E ListPRXH]) 1);
  10.182  by (etac List_ind 1);
  10.183  by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E ListPRXH])));
  10.184 -val ListPR_wf = result();
  10.185 +qed "ListPR_wf";
  10.186  
    11.1 --- a/src/CCL/coinduction.ML	Wed Nov 30 13:18:42 1994 +0100
    11.2 +++ b/src/CCL/coinduction.ML	Wed Nov 30 13:53:46 1994 +0100
    11.3 @@ -9,15 +9,15 @@
    11.4  val [mono,prem] = goal Lfp.thy "[| mono(f);  a : f(lfp(f)) |] ==> a : lfp(f)";
    11.5  by (rtac ((mono RS lfp_Tarski) RS ssubst) 1);
    11.6  by (rtac prem 1);
    11.7 -val lfpI = result();
    11.8 +qed "lfpI";
    11.9  
   11.10  val prems = goal CCL.thy "[| a=a';  a' : A |] ==> a : A";
   11.11  by (simp_tac (term_ss addsimps prems) 1);
   11.12 -val ssubst_single = result();
   11.13 +qed "ssubst_single";
   11.14  
   11.15  val prems = goal CCL.thy "[| a=a';  b=b';  <a',b'> : A |] ==> <a,b> : A";
   11.16  by (simp_tac (term_ss addsimps prems) 1);
   11.17 -val ssubst_pair = result();
   11.18 +qed "ssubst_pair";
   11.19  
   11.20  (***)
   11.21  
   11.22 @@ -42,7 +42,7 @@
   11.23  
   11.24  goal Term.thy "<a,a> : PO";
   11.25  by (rtac (po_refl RS (XH_to_D PO_iff)) 1);
   11.26 -val PO_refl = result();
   11.27 +qed "PO_refl";
   11.28  
   11.29  val POgenIs = map (mk_genIs Term.thy data_defs POgenXH POgen_mono)
   11.30        ["<true,true> : POgen(R)",
   11.31 @@ -72,7 +72,7 @@
   11.32  
   11.33  goal Term.thy "<a,a> : EQ";
   11.34  by (rtac (refl RS (EQ_iff RS iffD1)) 1);
   11.35 -val EQ_refl = result();
   11.36 +qed "EQ_refl";
   11.37  
   11.38  val EQgenIs = map (mk_genIs Term.thy data_defs EQgenXH EQgen_mono)
   11.39  ["<true,true> : EQgen(R)",
    12.1 --- a/src/CCL/equalities.ML	Wed Nov 30 13:18:42 1994 +0100
    12.2 +++ b/src/CCL/equalities.ML	Wed Nov 30 13:53:46 1994 +0100
    12.3 @@ -17,118 +17,118 @@
    12.4  
    12.5  goal Set.thy "A Int A = A";
    12.6  by (fast_tac eq_cs 1);
    12.7 -val Int_absorb = result();
    12.8 +qed "Int_absorb";
    12.9  
   12.10  goal Set.thy "A Int B  =  B Int A";
   12.11  by (fast_tac eq_cs 1);
   12.12 -val Int_commute = result();
   12.13 +qed "Int_commute";
   12.14  
   12.15  goal Set.thy "(A Int B) Int C  =  A Int (B Int C)";
   12.16  by (fast_tac eq_cs 1);
   12.17 -val Int_assoc = result();
   12.18 +qed "Int_assoc";
   12.19  
   12.20  goal Set.thy "(A Un B) Int C  =  (A Int C) Un (B Int C)";
   12.21  by (fast_tac eq_cs 1);
   12.22 -val Int_Un_distrib = result();
   12.23 +qed "Int_Un_distrib";
   12.24  
   12.25  goal Set.thy "(A<=B) <-> (A Int B = A)";
   12.26  by (fast_tac (eq_cs addSEs [equalityE]) 1);
   12.27 -val subset_Int_eq = result();
   12.28 +qed "subset_Int_eq";
   12.29  
   12.30  (** Binary Union **)
   12.31  
   12.32  goal Set.thy "A Un A = A";
   12.33  by (fast_tac eq_cs 1);
   12.34 -val Un_absorb = result();
   12.35 +qed "Un_absorb";
   12.36  
   12.37  goal Set.thy "A Un B  =  B Un A";
   12.38  by (fast_tac eq_cs 1);
   12.39 -val Un_commute = result();
   12.40 +qed "Un_commute";
   12.41  
   12.42  goal Set.thy "(A Un B) Un C  =  A Un (B Un C)";
   12.43  by (fast_tac eq_cs 1);
   12.44 -val Un_assoc = result();
   12.45 +qed "Un_assoc";
   12.46  
   12.47  goal Set.thy "(A Int B) Un C  =  (A Un C) Int (B Un C)";
   12.48  by (fast_tac eq_cs 1);
   12.49 -val Un_Int_distrib = result();
   12.50 +qed "Un_Int_distrib";
   12.51  
   12.52  goal Set.thy
   12.53   "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
   12.54  by (fast_tac eq_cs 1);
   12.55 -val Un_Int_crazy = result();
   12.56 +qed "Un_Int_crazy";
   12.57  
   12.58  goal Set.thy "(A<=B) <-> (A Un B = B)";
   12.59  by (fast_tac (eq_cs addSEs [equalityE]) 1);
   12.60 -val subset_Un_eq = result();
   12.61 +qed "subset_Un_eq";
   12.62  
   12.63  (** Simple properties of Compl -- complement of a set **)
   12.64  
   12.65  goal Set.thy "A Int Compl(A) = {x.False}";
   12.66  by (fast_tac eq_cs 1);
   12.67 -val Compl_disjoint = result();
   12.68 +qed "Compl_disjoint";
   12.69  
   12.70  goal Set.thy "A Un Compl(A) = {x.True}";
   12.71  by (fast_tac eq_cs 1);
   12.72 -val Compl_partition = result();
   12.73 +qed "Compl_partition";
   12.74  
   12.75  goal Set.thy "Compl(Compl(A)) = A";
   12.76  by (fast_tac eq_cs 1);
   12.77 -val double_complement = result();
   12.78 +qed "double_complement";
   12.79  
   12.80  goal Set.thy "Compl(A Un B) = Compl(A) Int Compl(B)";
   12.81  by (fast_tac eq_cs 1);
   12.82 -val Compl_Un = result();
   12.83 +qed "Compl_Un";
   12.84  
   12.85  goal Set.thy "Compl(A Int B) = Compl(A) Un Compl(B)";
   12.86  by (fast_tac eq_cs 1);
   12.87 -val Compl_Int = result();
   12.88 +qed "Compl_Int";
   12.89  
   12.90  goal Set.thy "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))";
   12.91  by (fast_tac eq_cs 1);
   12.92 -val Compl_UN = result();
   12.93 +qed "Compl_UN";
   12.94  
   12.95  goal Set.thy "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))";
   12.96  by (fast_tac eq_cs 1);
   12.97 -val Compl_INT = result();
   12.98 +qed "Compl_INT";
   12.99  
  12.100  (*Halmos, Naive Set Theory, page 16.*)
  12.101  
  12.102  goal Set.thy "((A Int B) Un C = A Int (B Un C)) <-> (C<=A)";
  12.103  by (fast_tac (eq_cs addSEs [equalityE]) 1);
  12.104 -val Un_Int_assoc_eq = result();
  12.105 +qed "Un_Int_assoc_eq";
  12.106  
  12.107  
  12.108  (** Big Union and Intersection **)
  12.109  
  12.110  goal Set.thy "Union(A Un B) = Union(A) Un Union(B)";
  12.111  by (fast_tac eq_cs 1);
  12.112 -val Union_Un_distrib = result();
  12.113 +qed "Union_Un_distrib";
  12.114  
  12.115  val prems = goal Set.thy
  12.116     "(Union(C) Int A = {x.False}) <-> (ALL B:C. B Int A = {x.False})";
  12.117  by (fast_tac (eq_cs addSEs [equalityE]) 1);
  12.118 -val Union_disjoint = result();
  12.119 +qed "Union_disjoint";
  12.120  
  12.121  goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)";
  12.122  by (best_tac eq_cs 1);
  12.123 -val Inter_Un_distrib = result();
  12.124 +qed "Inter_Un_distrib";
  12.125  
  12.126  (** Unions and Intersections of Families **)
  12.127  
  12.128  goal Set.thy "(UN x:A. B(x)) = Union({Y. EX x:A. Y=B(x)})";
  12.129  by (fast_tac eq_cs 1);
  12.130 -val UN_eq = result();
  12.131 +qed "UN_eq";
  12.132  
  12.133  (*Look: it has an EXISTENTIAL quantifier*)
  12.134  goal Set.thy "(INT x:A. B(x)) = Inter({Y. EX x:A. Y=B(x)})";
  12.135  by (fast_tac eq_cs 1);
  12.136 -val INT_eq = result();
  12.137 +qed "INT_eq";
  12.138  
  12.139  goal Set.thy "A Int Union(B) = (UN C:B. A Int C)";
  12.140  by (fast_tac eq_cs 1);
  12.141 -val Int_Union_image = result();
  12.142 +qed "Int_Union_image";
  12.143  
  12.144  goal Set.thy "A Un Inter(B) = (INT C:B. A Un C)";
  12.145  by (fast_tac eq_cs 1);
  12.146 -val Un_Inter_image = result();
  12.147 +qed "Un_Inter_image";
    13.1 --- a/src/CCL/eval.ML	Wed Nov 30 13:18:42 1994 +0100
    13.2 +++ b/src/CCL/eval.ML	Wed Nov 30 13:53:46 1994 +0100
    13.3 @@ -16,7 +16,7 @@
    13.4  val prems = goalw thy [apply_def]
    13.5     "[| f ---> lam x.b(x);  b(a) ---> c |] ==> f ` a ---> c";
    13.6  by (ceval_tac prems);
    13.7 -val applyV = result();
    13.8 +qed "applyV";
    13.9  
   13.10  EVal_rls := !EVal_rls @ [applyV];
   13.11  
   13.12 @@ -25,20 +25,20 @@
   13.13  by (rtac (major RS canonical) 1);
   13.14  by (REPEAT (DEPTH_SOLVE_1 (resolve_tac ([major]@prems@(!EVal_rls)) 1 ORELSE
   13.15                             etac substitute 1)));
   13.16 -val letV = result();
   13.17 +qed "letV";
   13.18  
   13.19  val prems = goalw thy [fix_def]
   13.20     "f(fix(f)) ---> c ==> fix(f) ---> c";
   13.21  by (rtac applyV 1);
   13.22  by (rtac lamV 1);
   13.23  by (resolve_tac prems 1);
   13.24 -val fixV = result();
   13.25 +qed "fixV";
   13.26  
   13.27  val prems = goalw thy [letrec_def]
   13.28      "h(t,%y.letrec g x be h(x,g) in g(y)) ---> c ==> \
   13.29  \                  letrec g x be h(x,g) in g(t) ---> c";
   13.30  by (REPEAT (resolve_tac (prems @ [fixV,applyV,lamV]) 1));
   13.31 -val letrecV = result();
   13.32 +qed "letrecV";
   13.33  
   13.34  EVal_rls := !EVal_rls @ [letV,letrecV,fixV];
   13.35  
    14.1 --- a/src/CCL/ex/List.ML	Wed Nov 30 13:18:42 1994 +0100
    14.2 +++ b/src/CCL/ex/List.ML	Wed Nov 30 13:53:46 1994 +0100
    14.3 @@ -34,52 +34,52 @@
    14.4  val [prem] = goal List.thy "n:Nat ==> map(f) ^ n ` [] = []";
    14.5  br (prem RS Nat_ind) 1;
    14.6  by (ALLGOALS (asm_simp_tac list_ss));
    14.7 -val nmapBnil = result();
    14.8 +qed "nmapBnil";
    14.9  
   14.10  val [prem] = goal List.thy "n:Nat ==> map(f)^n`(x$xs) = (f^n`x)$(map(f)^n`xs)";
   14.11  br (prem RS Nat_ind) 1;
   14.12  by (ALLGOALS (asm_simp_tac list_ss));
   14.13 -val nmapBcons = result();
   14.14 +qed "nmapBcons";
   14.15  
   14.16  (***)
   14.17  
   14.18  val prems = goalw List.thy [map_def]
   14.19    "[| !!x.x:A==>f(x):B;  l : List(A) |] ==> map(f,l) : List(B)";
   14.20  by (typechk_tac prems 1);
   14.21 -val mapT = result();
   14.22 +qed "mapT";
   14.23  
   14.24  val prems = goalw List.thy [append_def]
   14.25    "[| l : List(A);  m : List(A) |] ==> l @ m : List(A)";
   14.26  by (typechk_tac prems 1);
   14.27 -val appendT = result();
   14.28 +qed "appendT";
   14.29  
   14.30  val prems = goal List.thy
   14.31    "[| l : {l:List(A). m : {m:List(A).P(l @ m)}} |] ==> l @ m : {x:List(A). P(x)}";
   14.32  by (cut_facts_tac prems 1);
   14.33  by (fast_tac (set_cs addSIs [SubtypeI,appendT] addSEs [SubtypeE]) 1);
   14.34 -val appendTS = result();
   14.35 +qed "appendTS";
   14.36  
   14.37  val prems = goalw List.thy [filter_def]
   14.38    "[| f:A->Bool;   l : List(A) |] ==> filter(f,l) : List(A)";
   14.39  by (typechk_tac prems 1);
   14.40 -val filterT = result();
   14.41 +qed "filterT";
   14.42  
   14.43  val prems = goalw List.thy [flat_def]
   14.44    "l : List(List(A)) ==> flat(l) : List(A)";
   14.45  by (typechk_tac (appendT::prems) 1);
   14.46 -val flatT = result();
   14.47 +qed "flatT";
   14.48  
   14.49  val prems = goalw List.thy [insert_def]
   14.50    "[|  f : A->A->Bool; a:A; l : List(A) |] ==> insert(f,a,l) : List(A)";
   14.51  by (typechk_tac prems 1);
   14.52 -val insertT = result();
   14.53 +qed "insertT";
   14.54  
   14.55  val prems = goal List.thy
   14.56    "[| f : {f:A->A->Bool. a : {a:A. l : {l:List(A).P(insert(f,a,l))}}} |] ==> \
   14.57  \  insert(f,a,l)  : {x:List(A). P(x)}";
   14.58  by (cut_facts_tac prems 1);
   14.59  by (fast_tac (set_cs addSIs [SubtypeI,insertT] addSEs [SubtypeE]) 1);
   14.60 -val insertTS = result();
   14.61 +qed "insertTS";
   14.62  
   14.63  val prems = goalw List.thy [partition_def]
   14.64    "[| f:A->Bool;  l : List(A) |] ==> partition(f,l) : List(A)*List(A)";
   14.65 @@ -88,7 +88,7 @@
   14.66  br (ListPRI RS wfstI RS (ListPR_wf RS wmap_wf RS wfI)) 2;
   14.67  br (ListPRI RS wfstI RS (ListPR_wf RS wmap_wf RS wfI)) 1;
   14.68  by (REPEAT (atac 1));
   14.69 -val partitionT = result();
   14.70 +qed "partitionT";
   14.71  
   14.72  (*** Correctness Conditions for Insertion Sort ***)
   14.73  
    15.1 --- a/src/CCL/ex/Nat.ML	Wed Nov 30 13:18:42 1994 +0100
    15.2 +++ b/src/CCL/ex/Nat.ML	Wed Nov 30 13:53:46 1994 +0100
    15.3 @@ -27,34 +27,34 @@
    15.4  val [prem] = goal Nat.thy "n:Nat ==> f^n`f(a) = f^succ(n)`a";
    15.5  br (prem RS Nat_ind) 1;
    15.6  by (ALLGOALS (asm_simp_tac nat_ss));
    15.7 -val napply_f = result();
    15.8 +qed "napply_f";
    15.9  
   15.10  (****)
   15.11  
   15.12  val prems = goalw Nat.thy [add_def] "[| a:Nat;  b:Nat |] ==> a #+ b : Nat";
   15.13  by (typechk_tac prems 1);
   15.14 -val addT = result();
   15.15 +qed "addT";
   15.16  
   15.17  val prems = goalw Nat.thy [mult_def] "[| a:Nat;  b:Nat |] ==> a #* b : Nat";
   15.18  by (typechk_tac (addT::prems) 1);
   15.19 -val multT = result();
   15.20 +qed "multT";
   15.21  
   15.22  (* Defined to return zero if a<b *)
   15.23  val prems = goalw Nat.thy [sub_def] "[| a:Nat;  b:Nat |] ==> a #- b : Nat";
   15.24  by (typechk_tac (prems) 1);
   15.25  by clean_ccs_tac;
   15.26  be (NatPRI RS wfstI RS (NatPR_wf RS wmap_wf RS wfI)) 1;
   15.27 -val subT = result();
   15.28 +qed "subT";
   15.29  
   15.30  val prems = goalw Nat.thy [le_def] "[| a:Nat;  b:Nat |] ==> a #<= b : Bool";
   15.31  by (typechk_tac (prems) 1);
   15.32  by clean_ccs_tac;
   15.33  be (NatPRI RS wfstI RS (NatPR_wf RS wmap_wf RS wfI)) 1;
   15.34 -val leT = result();
   15.35 +qed "leT";
   15.36  
   15.37  val prems = goalw Nat.thy [not_def,lt_def] "[| a:Nat;  b:Nat |] ==> a #< b : Bool";
   15.38  by (typechk_tac (prems@[leT]) 1);
   15.39 -val ltT = result();
   15.40 +qed "ltT";
   15.41  
   15.42  (* Correctness conditions for subtractive division **)
   15.43  
    16.1 --- a/src/CCL/ex/Stream.ML	Wed Nov 30 13:18:42 1994 +0100
    16.2 +++ b/src/CCL/ex/Stream.ML	Wed Nov 30 13:53:46 1994 +0100
    16.3 @@ -23,7 +23,7 @@
    16.4  by (EQgen_tac list_ss [] 1);
    16.5  by (simp_tac list_ss 1);
    16.6  by (fast_tac ccl_cs 1);
    16.7 -val map_comp = result();
    16.8 +qed "map_comp";
    16.9  
   16.10  (*** Mapping the identity function leaves a list unchanged ***)
   16.11  
   16.12 @@ -35,7 +35,7 @@
   16.13  be (XH_to_E ListsXH) 1;
   16.14  by (EQgen_tac list_ss [] 1);
   16.15  by (fast_tac ccl_cs 1);
   16.16 -val map_id = result();
   16.17 +qed "map_id";
   16.18  
   16.19  (*** Mapping distributes over append ***)
   16.20  
   16.21 @@ -50,7 +50,7 @@
   16.22  be (XH_to_E ListsXH) 1;
   16.23  by (EQgen_tac list_ss [] 1);
   16.24  by (fast_tac ccl_cs 1);
   16.25 -val map_append = result();
   16.26 +qed "map_append";
   16.27  
   16.28  (*** Append is associative ***)
   16.29  
   16.30 @@ -67,7 +67,7 @@
   16.31  be (XH_to_E ListsXH) 1;
   16.32  by (EQgen_tac list_ss [] 1);
   16.33  by (fast_tac ccl_cs 1);
   16.34 -val append_assoc = result();
   16.35 +qed "append_assoc";
   16.36  
   16.37  (*** Appending anything to an infinite list doesn't alter it ****)
   16.38  
   16.39 @@ -78,7 +78,7 @@
   16.40  be (XH_to_E IListsXH) 1;
   16.41  by (EQgen_tac list_ss [] 1);
   16.42  by (fast_tac ccl_cs 1);
   16.43 -val ilist_append = result();
   16.44 +qed "ilist_append";
   16.45  
   16.46  (*** The equivalance of two versions of an iteration function       ***)
   16.47  (*                                                                    *)
   16.48 @@ -88,18 +88,18 @@
   16.49  goalw Stream.thy [iter1_def] "iter1(f,a) = a$iter1(f,f(a))";
   16.50  br (letrecB RS trans) 1;
   16.51  by (simp_tac term_ss 1);
   16.52 -val iter1B = result();
   16.53 +qed "iter1B";
   16.54  
   16.55  goalw Stream.thy [iter2_def] "iter2(f,a) = a $ map(f,iter2(f,a))";
   16.56  br (letrecB RS trans) 1;
   16.57  br refl 1;
   16.58 -val iter2B = result();
   16.59 +qed "iter2B";
   16.60  
   16.61  val [prem] =goal Stream.thy
   16.62     "n:Nat ==> map(f) ^ n ` iter2(f,a) = (f ^ n ` a) $ (map(f) ^ n ` map(f,iter2(f,a)))";
   16.63  br (iter2B RS ssubst) 1;back();back();
   16.64  by (simp_tac (list_ss addsimps [prem RS nmapBcons]) 1);
   16.65 -val iter2Blemma = result();
   16.66 +qed "iter2Blemma";
   16.67  
   16.68  goal Stream.thy "iter1(f,a) = iter2(f,a)";
   16.69  by (eq_coinduct3_tac 
   16.70 @@ -111,4 +111,4 @@
   16.71  by (rtac (napply_f RS ssubst) 1 THEN atac 1);
   16.72  by (res_inst_tac [("f1","f")] (napplyBsucc RS subst) 1);
   16.73  by (fast_tac type_cs 1);
   16.74 -val iter1_iter2_eq = result();
   16.75 +qed "iter1_iter2_eq";
    17.1 --- a/src/CCL/genrec.ML	Wed Nov 30 13:18:42 1994 +0100
    17.2 +++ b/src/CCL/genrec.ML	Wed Nov 30 13:53:46 1994 +0100
    17.3 @@ -20,12 +20,12 @@
    17.4  by (rtac ballI 1);
    17.5  by (etac (spec RS mp RS mp) 1);
    17.6  by (REPEAT (eresolve_tac [SubtypeD1,SubtypeD2] 1));
    17.7 -val letrecT = result();
    17.8 +qed "letrecT";
    17.9  
   17.10  goalw Wfd.thy [SPLIT_def] "SPLIT(<a,b>,B) = B(a,b)";
   17.11  by (rtac set_ext 1);
   17.12  by (fast_tac ccl_cs 1);
   17.13 -val SPLITB = result();
   17.14 +qed "SPLITB";
   17.15  
   17.16  val prems = goalw Wfd.thy [letrec2_def]
   17.17      "[| a : A;  b : B;  \
   17.18 @@ -40,11 +40,11 @@
   17.19  by (rtac (SPLITB RS subst) 1);
   17.20  by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE 
   17.21              eresolve_tac [bspec,SubtypeE,sym RS subst] 1));
   17.22 -val letrec2T = result();
   17.23 +qed "letrec2T";
   17.24  
   17.25  goal Wfd.thy "SPLIT(<a,<b,c>>,%x xs.SPLIT(xs,%y z.B(x,y,z))) = B(a,b,c)";
   17.26  by (simp_tac (ccl_ss addsimps [SPLITB]) 1);
   17.27 -val lemma = result();
   17.28 +qed "lemma";
   17.29  
   17.30  val prems = goalw Wfd.thy [letrec3_def]
   17.31      "[| a : A;  b : B;  c : C;  \
   17.32 @@ -60,7 +60,7 @@
   17.33  by (rtac (lemma RS subst) 1);
   17.34  by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE 
   17.35              eresolve_tac [bspec,SubtypeE,sym RS subst] 1));
   17.36 -val letrec3T = result();
   17.37 +qed "letrec3T";
   17.38  
   17.39  val letrecTs = [letrecT,letrec2T,letrec3T];
   17.40  
   17.41 @@ -72,14 +72,14 @@
   17.42  \       g(a) : D(a) ==> g(a) : E;  a:A;  <a,p>:wf(R) |] ==> \
   17.43  \   g(a) : E";
   17.44  by (REPEAT (ares_tac ([SubtypeI,major RS bspec,major]@prems) 1));
   17.45 -val rcallT = result();
   17.46 +qed "rcallT";
   17.47  
   17.48  val major::prems = goal Wfd.thy
   17.49      "[| ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
   17.50  \       g(a,b) : D(a,b) ==> g(a,b) : E;  a:A;  b:B;  <<a,b>,<p,q>>:wf(R) |] ==> \
   17.51  \   g(a,b) : E";
   17.52  by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec,major]@prems) 1));
   17.53 -val rcall2T = result();
   17.54 +qed "rcall2T";
   17.55  
   17.56  val major::prems = goal Wfd.thy
   17.57      "[| 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); \
   17.58 @@ -87,7 +87,7 @@
   17.59  \       a:A;  b:B;  c:C;  <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==> \
   17.60  \   g(a,b,c) : E";
   17.61  by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec RS bspec,major]@prems) 1));
   17.62 -val rcall3T = result();
   17.63 +qed "rcall3T";
   17.64  
   17.65  val rcallTs = [rcallT,rcall2T,rcall3T];
   17.66  
   17.67 @@ -113,7 +113,7 @@
   17.68  by (resolve_tac (prems RL [sym]) 1);
   17.69  by (rtac rcallT 1);
   17.70  by (REPEAT (ares_tac prems 1));
   17.71 -val hyprcallT = result();
   17.72 +qed "hyprcallT";
   17.73  
   17.74  val prems = goal Wfd.thy
   17.75      "[| g(a,b) = c; ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
   17.76 @@ -124,7 +124,7 @@
   17.77  by (resolve_tac (prems RL [sym]) 1);
   17.78  by (rtac rcall2T 1);
   17.79  by (REPEAT (ares_tac prems 1));
   17.80 -val hyprcall2T = result();
   17.81 +qed "hyprcall2T";
   17.82  
   17.83  val prems = goal Wfd.thy
   17.84    "[| g(a,b,c) = d; \
   17.85 @@ -136,7 +136,7 @@
   17.86  by (resolve_tac (prems RL [sym]) 1);
   17.87  by (rtac rcall3T 1);
   17.88  by (REPEAT (ares_tac prems 1));
   17.89 -val hyprcall3T = result();
   17.90 +qed "hyprcall3T";
   17.91  
   17.92  val hyprcallTs = [hyprcallT,hyprcall2T,hyprcall3T];
   17.93  
   17.94 @@ -146,20 +146,20 @@
   17.95      "[| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); P |] ==> \
   17.96  \    P";
   17.97  by (REPEAT (ares_tac prems 1));
   17.98 -val rmIH1  = result();
   17.99 +qed "rmIH1";
  17.100  
  17.101  val prems = goal Wfd.thy
  17.102      "[| ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P |] ==> \
  17.103  \    P";
  17.104  by (REPEAT (ares_tac prems 1));
  17.105 -val rmIH2  = result();
  17.106 +qed "rmIH2";
  17.107  
  17.108  val prems = goal Wfd.thy
  17.109   "[| 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); \
  17.110  \    P |] ==> \
  17.111  \    P";
  17.112  by (REPEAT (ares_tac prems 1));
  17.113 -val rmIH3  = result();
  17.114 +qed "rmIH3";
  17.115  
  17.116  val rmIHs = [rmIH1,rmIH2,rmIH3];
  17.117  
    18.1 --- a/src/CCL/mono.ML	Wed Nov 30 13:18:42 1994 +0100
    18.2 +++ b/src/CCL/mono.ML	Wed Nov 30 13:53:46 1994 +0100
    18.3 @@ -13,34 +13,34 @@
    18.4  
    18.5  val prems = goal Set.thy "A<=B ==> Union(A) <= Union(B)";
    18.6  by (cfast_tac prems 1);
    18.7 -val Union_mono = result();
    18.8 +qed "Union_mono";
    18.9  
   18.10  val prems = goal Set.thy "[| B<=A |] ==> Inter(A) <= Inter(B)";
   18.11  by (cfast_tac prems 1);
   18.12 -val Inter_anti_mono = result();
   18.13 +qed "Inter_anti_mono";
   18.14  
   18.15  val prems = goal Set.thy
   18.16      "[| A<=B;  !!x. x:A ==> f(x)<=g(x) |] ==> \
   18.17  \    (UN x:A. f(x)) <= (UN x:B. g(x))";
   18.18  by (REPEAT (eresolve_tac [UN_E,ssubst] 1
   18.19       ORELSE ares_tac ((prems RL [subsetD]) @ [subsetI,UN_I]) 1));
   18.20 -val UN_mono = result();
   18.21 +qed "UN_mono";
   18.22  
   18.23  val prems = goal Set.thy
   18.24      "[| B<=A;  !!x. x:A ==> f(x)<=g(x) |] ==> \
   18.25  \    (INT x:A. f(x)) <= (INT x:A. g(x))";
   18.26  by (REPEAT (ares_tac ((prems RL [subsetD]) @ [subsetI,INT_I]) 1
   18.27       ORELSE etac INT_D 1));
   18.28 -val INT_anti_mono = result();
   18.29 +qed "INT_anti_mono";
   18.30  
   18.31  val prems = goal Set.thy "[| A<=C;  B<=D |] ==> A Un B <= C Un D";
   18.32  by (cfast_tac prems 1);
   18.33 -val Un_mono = result();
   18.34 +qed "Un_mono";
   18.35  
   18.36  val prems = goal Set.thy "[| A<=C;  B<=D |] ==> A Int B <= C Int D";
   18.37  by (cfast_tac prems 1);
   18.38 -val Int_mono = result();
   18.39 +qed "Int_mono";
   18.40  
   18.41  val prems = goal Set.thy "[| A<=B |] ==> Compl(B) <= Compl(A)";
   18.42  by (cfast_tac prems 1);
   18.43 -val Compl_anti_mono = result();
   18.44 +qed "Compl_anti_mono";
    19.1 --- a/src/CCL/subset.ML	Wed Nov 30 13:18:42 1994 +0100
    19.2 +++ b/src/CCL/subset.ML	Wed Nov 30 13:53:46 1994 +0100
    19.3 @@ -15,13 +15,13 @@
    19.4  val prems = goal Set.thy
    19.5      "B:A ==> B <= Union(A)";
    19.6  by (REPEAT (ares_tac (prems@[subsetI,UnionI]) 1));
    19.7 -val Union_upper = result();
    19.8 +qed "Union_upper";
    19.9  
   19.10  val prems = goal Set.thy
   19.11      "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C";
   19.12  by (REPEAT (ares_tac [subsetI] 1
   19.13       ORELSE eresolve_tac ([UnionE] @ (prems RL [subsetD])) 1));
   19.14 -val Union_least = result();
   19.15 +qed "Union_least";
   19.16  
   19.17  
   19.18  (*** Big Intersection -- greatest lower bound of a set ***)
   19.19 @@ -30,70 +30,70 @@
   19.20      "B:A ==> Inter(A) <= B";
   19.21  by (REPEAT (resolve_tac (prems@[subsetI]) 1
   19.22       ORELSE etac InterD 1));
   19.23 -val Inter_lower = result();
   19.24 +qed "Inter_lower";
   19.25  
   19.26  val prems = goal Set.thy
   19.27      "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)";
   19.28  by (REPEAT (ares_tac [subsetI,InterI] 1
   19.29       ORELSE eresolve_tac (prems RL [subsetD]) 1));
   19.30 -val Inter_greatest = result();
   19.31 +qed "Inter_greatest";
   19.32  
   19.33  (*** Finite Union -- the least upper bound of 2 sets ***)
   19.34  
   19.35  goal Set.thy "A <= A Un B";
   19.36  by (REPEAT (ares_tac [subsetI,UnI1] 1));
   19.37 -val Un_upper1 = result();
   19.38 +qed "Un_upper1";
   19.39  
   19.40  goal Set.thy "B <= A Un B";
   19.41  by (REPEAT (ares_tac [subsetI,UnI2] 1));
   19.42 -val Un_upper2 = result();
   19.43 +qed "Un_upper2";
   19.44  
   19.45  val prems = goal Set.thy "[| A<=C;  B<=C |] ==> A Un B <= C";
   19.46  by (cut_facts_tac prems 1);
   19.47  by (DEPTH_SOLVE (ares_tac [subsetI] 1 
   19.48            ORELSE eresolve_tac [UnE,subsetD] 1));
   19.49 -val Un_least = result();
   19.50 +qed "Un_least";
   19.51  
   19.52  (*** Finite Intersection -- the greatest lower bound of 2 sets *)
   19.53  
   19.54  goal Set.thy "A Int B <= A";
   19.55  by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1));
   19.56 -val Int_lower1 = result();
   19.57 +qed "Int_lower1";
   19.58  
   19.59  goal Set.thy "A Int B <= B";
   19.60  by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1));
   19.61 -val Int_lower2 = result();
   19.62 +qed "Int_lower2";
   19.63  
   19.64  val prems = goal Set.thy "[| C<=A;  C<=B |] ==> C <= A Int B";
   19.65  by (cut_facts_tac prems 1);
   19.66  by (REPEAT (ares_tac [subsetI,IntI] 1
   19.67       ORELSE etac subsetD 1));
   19.68 -val Int_greatest = result();
   19.69 +qed "Int_greatest";
   19.70  
   19.71  (*** Monotonicity ***)
   19.72  
   19.73  val [prem] = goalw Set.thy [mono_def]
   19.74      "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)";
   19.75  by (REPEAT (ares_tac [allI, impI, prem] 1));
   19.76 -val monoI = result();
   19.77 +qed "monoI";
   19.78  
   19.79  val [major,minor] = goalw Set.thy [mono_def]
   19.80      "[| mono(f);  A <= B |] ==> f(A) <= f(B)";
   19.81  by (rtac (major RS spec RS spec RS mp) 1);
   19.82  by (rtac minor 1);
   19.83 -val monoD = result();
   19.84 +qed "monoD";
   19.85  
   19.86  val [prem] = goal Set.thy "mono(f) ==> f(A) Un f(B) <= f(A Un B)";
   19.87  by (rtac Un_least 1);
   19.88  by (rtac (Un_upper1 RS (prem RS monoD)) 1);
   19.89  by (rtac (Un_upper2 RS (prem RS monoD)) 1);
   19.90 -val mono_Un = result();
   19.91 +qed "mono_Un";
   19.92  
   19.93  val [prem] = goal Set.thy "mono(f) ==> f(A Int B) <= f(A) Int f(B)";
   19.94  by (rtac Int_greatest 1);
   19.95  by (rtac (Int_lower1 RS (prem RS monoD)) 1);
   19.96  by (rtac (Int_lower2 RS (prem RS monoD)) 1);
   19.97 -val mono_Int = result();
   19.98 +qed "mono_Int";
   19.99  
  19.100  (****)
  19.101  
    20.1 --- a/src/CCL/typecheck.ML	Wed Nov 30 13:18:42 1994 +0100
    20.2 +++ b/src/CCL/typecheck.ML	Wed Nov 30 13:53:46 1994 +0100
    20.3 @@ -46,23 +46,23 @@
    20.4  by (cut_facts_tac prems 1);
    20.5  by (etac (letB RS ssubst) 1);
    20.6  by (assume_tac 1);
    20.7 -val letT = result();
    20.8 +qed "letT";
    20.9  
   20.10  val prems = goal Type.thy
   20.11       "[| a:A;  f : Pi(A,B)  |] ==> f ` a  : B(a)";
   20.12  by (REPEAT (ares_tac (applyT::prems) 1));
   20.13 -val applyT2 = result();
   20.14 +qed "applyT2";
   20.15  
   20.16  val prems = goal Type.thy 
   20.17      "[| a:A;  a:A ==> P(a) |] ==> a : {x:A.P(x)}";
   20.18  by (fast_tac (type_cs addSIs prems) 1);
   20.19 -val rcall_lemma1 = result();
   20.20 +qed "rcall_lemma1";
   20.21  
   20.22  val prems = goal Type.thy 
   20.23      "[| a:{x:A.Q(x)};  [| a:A; Q(a) |] ==> P(a) |] ==> a : {x:A.P(x)}";
   20.24  by (cut_facts_tac prems 1);
   20.25  by (fast_tac (type_cs addSIs prems) 1);
   20.26 -val rcall_lemma2 = result();
   20.27 +qed "rcall_lemma2";
   20.28  
   20.29  val rcall_lemmas = [asm_rl,rcall_lemma1,SubtypeD1,rcall_lemma2];
   20.30