ex/rel.ML

--- a/ex/rel.ML	Fri Nov 11 10:35:03 1994 +0100
+++ b/ex/rel.ML	Mon Nov 21 17:50:34 1994 +0100
@@ -35,46 +35,46 @@
 
 val [prem] = goalw Rel.thy [domain_def,Pair_def] "<a,b>: r ==> a : domain(r)";
 by (fast_tac (set_cs addIs [prem]) 1);
-val domainI = result();
+qed "domainI";
 
 val major::prems = goalw Rel.thy [domain_def]
     "[| a : domain(r);  !!y. <a,y>: r ==> P |] ==> P";
 by (rtac (major RS CollectE) 1);
 by (etac exE 1);
 by (REPEAT (ares_tac prems 1));
-val domainE = result();
+qed "domainE";
 
 
 (*** range2 ***)
 
 val [prem] = goalw Rel.thy [range2_def,Pair_def] "<a,b>: r ==> b : range2(r)";
 by (fast_tac (set_cs addIs [prem]) 1);
-val range2I = result();
+qed "range2I";
 
 val major::prems = goalw Rel.thy [range2_def]
     "[| b : range2(r);  !!x. <x,b>: r ==> P |] ==> P";
 by (rtac (major RS CollectE) 1);
 by (etac exE 1);
 by (REPEAT (ares_tac prems 1));
-val range2E = result();
+qed "range2E";
 
 
 (*** field ***)
 
 val [prem] = goalw Rel.thy [field_def] "<a,b>: r ==> a : field(r)";
 by (rtac (prem RS domainI RS UnI1) 1);
-val fieldI1 = result();
+qed "fieldI1";
 
 val [prem] = goalw Rel.thy [field_def] "<a,b>: r ==> b : field(r)";
 by (rtac (prem RS range2I RS UnI2) 1);
-val fieldI2 = result();
+qed "fieldI2";
 
 val [prem] = goalw Rel.thy [field_def]
     "(~ <c,a>:r ==> <a,b>: r) ==> a : field(r)";
 by (rtac (prem RS domainI RS UnCI) 1);
 by (swap_res_tac [range2I] 1);
 by (etac notnotD 1);
-val fieldCI = result();
+qed "fieldCI";
 
 val major::prems = goalw Rel.thy [field_def]
      "[| a : field(r);  \
@@ -82,15 +82,15 @@
 \        !!x. <x,a>: r ==> P        |] ==> P";
 by (rtac (major RS UnE) 1);
 by (REPEAT (eresolve_tac (prems@[domainE,range2E]) 1));
-val fieldE = result();
+qed "fieldE";
 
 goalw Rel.thy [field_def] "domain(r) <= field(r)";
 by (rtac Un_upper1 1);
-val domain_in_field = result();
+qed "domain_in_field";
 
 goalw Rel.thy [field_def] "range2(r) <= field(r)";
 by (rtac Un_upper2 1);
-val range2_in_field = result();
+qed "range2_in_field";
 
 
 ????????????????????????????????????????????????????????????????;
@@ -105,5 +105,5 @@
 by (fast_tac ZF_cs 3);
 by (fast_tac ZF_cs 2);
 by (fast_tac ZF_cs 1);
-val wfI2 = result();
+qed "wfI2";