ex/Acc.ML

--- a/ex/Acc.ML	Fri Nov 11 10:35:03 1994 +0100
+++ b/ex/Acc.ML	Mon Nov 21 17:50:34 1994 +0100
@@ -16,13 +16,13 @@
     "[| !!b. <b,a>:r ==> b: acc(r) |] ==> a: acc(r)";
 by (fast_tac (set_cs addIs (prems @ 
 			    map (rewrite_rule [pred_def]) acc.intrs)) 1);
-val accI = result();
+qed "accI";
 
 goal Acc.thy "!!a b r. [| b: acc(r);  <a,b>: r |] ==> a: acc(r)";
 by (etac acc.elim 1);
 by (rewtac pred_def);
 by (fast_tac set_cs 1);
-val acc_downward = result();
+qed "acc_downward";
 
 val [major,indhyp] = goal Acc.thy
     "[| a : acc(r);						\
@@ -34,7 +34,7 @@
 by (rewtac pred_def);
 by (fast_tac set_cs 2);
 be (Int_lower1 RS Pow_mono RS subsetD) 1;
-val acc_induct = result();
+qed "acc_induct";
 
 
 val [major] = goal Acc.thy "r <= Sigma(acc(r), %u. acc(r)) ==> wf(r)";
@@ -42,22 +42,22 @@
 by (etac acc.induct 1);
 by (rewtac pred_def);
 by (fast_tac set_cs 1);
-val acc_wfI = result();
+qed "acc_wfI";
 
 val [major] = goal Acc.thy "wf(r) ==> ALL x. <x,y>: r | <y,x>:r --> y: acc(r)";
 by (rtac (major RS wf_induct) 1);
 br (impI RS allI) 1;
 br accI 1;
 by (fast_tac set_cs 1);
-val acc_wfD_lemma = result();
+qed "acc_wfD_lemma";
 
 val [major] = goal Acc.thy "wf(r) ==> r <= Sigma(acc(r), %u. acc(r))";
 by (rtac subsetI 1);
 by (res_inst_tac [("p", "x")] PairE 1);
 by (fast_tac (set_cs addSIs [SigmaI,
 			     major RS acc_wfD_lemma RS spec RS mp]) 1);
-val acc_wfD = result();
+qed "acc_wfD";
 
 goal Acc.thy "wf(r)  =  (r <= Sigma(acc(r), %u. acc(r)))";
 by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]);
-val wf_acc_iff = result();
+qed "wf_acc_iff";