ex/meson.ML

--- a/ex/meson.ML	Fri Nov 11 10:35:03 1994 +0100
+++ b/ex/meson.ML	Mon Nov 21 17:50:34 1994 +0100
@@ -61,7 +61,7 @@
     "! x. ? y. Q(x,y) ==> ? f. ! x. Q(x,f(x))";
 by (cut_facts_tac [major] 1);
 by (fast_tac (HOL_cs addEs [selectI]) 1);
-val choice = result();
+qed "choice";
 
 
 (***** Generating clauses for the Meson Proof Procedure *****)
@@ -83,7 +83,7 @@
 by (rtac notE 1);
 by (etac minor 2);
 by (ALLGOALS assume_tac);
-val make_neg_rule = result();
+qed "make_neg_rule";
 
 (*For Plaisted's "Postive refinement" of the MESON procedure*)
 val [major,minor] = goal HOL.thy "~P|Q ==> (P ==> Q)";
@@ -91,7 +91,7 @@
 by (rtac notE 1);
 by (rtac minor 2);
 by (ALLGOALS assume_tac);
-val make_refined_neg_rule = result();
+qed "make_refined_neg_rule";
 
 (*P should be a literal*)
 val [major,minor] = goal HOL.thy "P|Q ==> ((P==>~P) ==> Q)";
@@ -99,7 +99,7 @@
 by (rtac notE 1);
 by (etac minor 1);
 by (ALLGOALS assume_tac);
-val make_pos_rule = result();
+qed "make_pos_rule";
 
 (*** Generation of a goal clause -- put away the final literal ***)
 
@@ -107,13 +107,13 @@
 by (rtac notE 1);
 by (rtac minor 2);
 by (ALLGOALS (rtac major));
-val make_neg_goal = result();
+qed "make_neg_goal";
 
 val [major,minor] = goal HOL.thy "P ==> ((P==>~P) ==> False)";
 by (rtac notE 1);
 by (rtac minor 1);
 by (ALLGOALS (rtac major));
-val make_pos_goal = result();
+qed "make_pos_goal";
 
 
 (**** Lemmas for forward proof (like congruence rules) ****)
@@ -125,28 +125,28 @@
 by (rtac (major RS conjE) 1);
 by (rtac conjI 1);
 by (ALLGOALS (eresolve_tac prems));
-val conj_forward = result();
+qed "conj_forward";
 
 val major::prems = goal HOL.thy
     "[| P'|Q';  P' ==> P;  Q' ==> Q |] ==> P|Q";
 by (rtac (major RS disjE) 1);
 by (ALLGOALS (dresolve_tac prems));
 by (ALLGOALS (eresolve_tac [disjI1,disjI2]));
-val disj_forward = result();
+qed "disj_forward";
 
 val major::prems = goal HOL.thy
     "[| ! x. P'(x);  !!x. P'(x) ==> P(x) |] ==> ! x. P(x)";
 by (rtac allI 1);
 by (resolve_tac prems 1);
 by (rtac (major RS spec) 1);
-val all_forward = result();
+qed "all_forward";
 
 val major::prems = goal HOL.thy
     "[| ? x. P'(x);  !!x. P'(x) ==> P(x) |] ==> ? x. P(x)";
 by (rtac (major RS exE) 1);
 by (rtac exI 1);
 by (eresolve_tac prems 1);
-val ex_forward = result();
+qed "ex_forward";
 
 
 (**** Operators for forward proof ****)
@@ -263,7 +263,7 @@
 by (ALLGOALS (eresolve_tac prems));
 by (etac notE 1);
 by (assume_tac 1);
-val disj_forward2 = result();
+qed "disj_forward2";
 
 (*Forward proof, passing extra assumptions as theorems to the tactic*)
 fun forward_res2 nf hyps state =