--- 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 =