# HG changeset patch
# User paulson
# Date 903088955 -7200
# Node ID 3a92144827620956cfcad69ab7b59e0820f532ad
# Parent  7a8975451a896cf14af9cb51651e2b893c172626
Uses Goal instead of "goal...thy" to avoid theory problems

diff -r 7a8975451a89 -r 3a9214482762 src/HOL/ex/meson.ML
--- a/src/HOL/ex/meson.ML	Thu Aug 13 18:14:26 1998 +0200
+++ b/src/HOL/ex/meson.ML	Fri Aug 14 12:02:35 1998 +0200
@@ -13,6 +13,8 @@
 
 writeln"File HOL/ex/meson.";
 
+context HOL.thy;
+
 (*Prove theorems using fast_tac*)
 fun prove_fun s = 
     prove_goal HOL.thy s
@@ -72,7 +74,7 @@
 (*** Generation of contrapositives ***)
 
 (*Inserts negated disjunct after removing the negation; P is a literal*)
-val [major,minor] = goal HOL.thy "~P|Q ==> ((~P==>P) ==> Q)";
+val [major,minor] = Goal "~P|Q ==> ((~P==>P) ==> Q)";
 by (rtac (major RS disjE) 1);
 by (rtac notE 1);
 by (etac minor 2);
@@ -80,15 +82,12 @@
 qed "make_neg_rule";
 
 (*For Plaisted's "Postive refinement" of the MESON procedure*)
-val [major,minor] = goal HOL.thy "~P|Q ==> (P ==> Q)";
-by (rtac (major RS disjE) 1);
-by (rtac notE 1);
-by (rtac minor 2);
-by (ALLGOALS assume_tac);
+Goal "~P|Q ==> (P ==> Q)";
+by (Blast_tac 1);
 qed "make_refined_neg_rule";
 
 (*P should be a literal*)
-val [major,minor] = goal HOL.thy "P|Q ==> ((P==>~P) ==> Q)";
+val [major,minor] = Goal "P|Q ==> ((P==>~P) ==> Q)";
 by (rtac (major RS disjE) 1);
 by (rtac notE 1);
 by (etac minor 1);
@@ -97,13 +96,13 @@
 
 (*** Generation of a goal clause -- put away the final literal ***)
 
-val [major,minor] = goal HOL.thy "~P ==> ((~P==>P) ==> False)";
+val [major,minor] = Goal "~P ==> ((~P==>P) ==> False)";
 by (rtac notE 1);
 by (rtac minor 2);
 by (ALLGOALS (rtac major));
 qed "make_neg_goal";
 
-val [major,minor] = goal HOL.thy "P ==> ((P==>~P) ==> False)";
+val [major,minor] = Goal "P ==> ((P==>~P) ==> False)";
 by (rtac notE 1);
 by (rtac minor 1);
 by (ALLGOALS (rtac major));
@@ -114,28 +113,28 @@
 
 (*NOTE: could handle conjunctions (faster?) by
     nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *)
-val major::prems = goal HOL.thy
+val major::prems = Goal
     "[| P'&Q';  P' ==> P;  Q' ==> Q |] ==> P&Q";
 by (rtac (major RS conjE) 1);
 by (rtac conjI 1);
 by (ALLGOALS (eresolve_tac prems));
 qed "conj_forward";
 
-val major::prems = goal HOL.thy
+val major::prems = Goal
     "[| 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]));
 qed "disj_forward";
 
-val major::prems = goal HOL.thy
+val major::prems = Goal
     "[| ! 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);
 qed "all_forward";
 
-val major::prems = goal HOL.thy
+val major::prems = Goal
     "[| ? x. P'(x);  !!x. P'(x) ==> P(x) |] ==> ? x. P(x)";
 by (rtac (major RS exE) 1);
 by (rtac exI 1);
@@ -249,7 +248,7 @@
 (**** Removal of duplicate literals ****)
 
 (*Version for removal of duplicate literals*)
-val major::prems = goal HOL.thy
+val major::prems = Goal
     "[| P'|Q';  P' ==> P;  [| Q'; P==>False |] ==> Q |] ==> P|Q";
 by (rtac (major RS disjE) 1);
 by (rtac disjI1 1);
diff -r 7a8975451a89 -r 3a9214482762 src/HOL/ex/mesontest.ML
--- a/src/HOL/ex/mesontest.ML	Thu Aug 13 18:14:26 1998 +0200
+++ b/src/HOL/ex/mesontest.ML	Fri Aug 14 12:02:35 1998 +0200
@@ -21,7 +21,7 @@
 val horns = make_horns clauses;
 val goes = gocls clauses;
 
-goal HOL.thy "False";
+Goal "False";
 by (resolve_tac goes 1);
 keep_derivs := FullDeriv;
 
@@ -33,6 +33,8 @@
 
 writeln"File HOL/ex/meson-test.";
 
+context Fun.thy;
+
 (*Deep unifications can be required, esp. during transformation to clauses*)
 val orig_trace_bound = !Unify.trace_bound
 and orig_search_bound = !Unify.search_bound;
@@ -46,7 +48,7 @@
 
 
 writeln"Problem 25";
-goal HOL.thy "(? x. P x) &  \
+Goal "(? x. P x) &  \
 \       (! x. L x --> ~ (M x & R x)) &  \
 \       (! x. P x --> (M x & L x)) &   \
 \       ((! x. P x --> Q x) | (? x. P x & R x))  \
@@ -61,13 +63,13 @@
 val horns25 = make_horns clauses25;     (*16 Horn clauses*)
 val go25::_ = gocls clauses25;
 
-goal HOL.thy "False";
+Goal "False";
 by (rtac go25 1);
 by (depth_prolog_tac horns25);
 
 
 writeln"Problem 26";
-goal HOL.thy "((? x. p x) = (? x. q x)) &     \
+Goal "((? x. p x) = (? x. q x)) &     \
 \     (! x. ! y. p x & q y --> (r x = s y)) \
 \ --> ((! x. p x --> r x) = (! x. q x --> s x))";
 by (rtac ccontr 1);
@@ -80,14 +82,14 @@
 val horns26 = make_horns clauses26;                     (*24 Horn clauses*)
 val go26::_ = gocls clauses26;
 
-goal HOL.thy "False";
+Goal "False";
 by (rtac go26 1);
 by (depth_prolog_tac horns26);  (*1.4 secs*)
 (*Proof is of length 107!!*)
 
 
 writeln"Problem 43  NOW PROVED AUTOMATICALLY!!";  (*16 Horn clauses*)
-goal HOL.thy "(! x. ! y. q x y = (! z. p z x = (p z y::bool)))  \
+Goal "(! x. ! y. q x y = (! z. p z x = (p z y::bool)))  \
 \         --> (! x. (! y. q x y = (q y x::bool)))";
 by (rtac ccontr 1);
 val [prem43] = gethyps 1;
@@ -99,7 +101,7 @@
 val horns43 = make_horns clauses43;     (*16*)
 val go43::_ = gocls clauses43;
 
-goal HOL.thy "False";
+Goal "False";
 by (rtac go43 1);
 by (best_prolog_tac size_of_subgoals horns43);   (*1.6 secs*)
 
@@ -157,163 +159,163 @@
 
 writeln"Pelletier's examples";
 (*1*)
-goal HOL.thy "(P --> Q)  =  (~Q --> ~P)";
+Goal "(P --> Q)  =  (~Q --> ~P)";
 by (safe_meson_tac 1);
 result();
 
 (*2*)
-goal HOL.thy "(~ ~ P) =  P";
+Goal "(~ ~ P) =  P";
 by (safe_meson_tac 1);
 result();
 
 (*3*)
-goal HOL.thy "~(P-->Q) --> (Q-->P)";
+Goal "~(P-->Q) --> (Q-->P)";
 by (safe_meson_tac 1);
 result();
 
 (*4*)
-goal HOL.thy "(~P-->Q)  =  (~Q --> P)";
+Goal "(~P-->Q)  =  (~Q --> P)";
 by (safe_meson_tac 1);
 result();
 
 (*5*)
-goal HOL.thy "((P|Q)-->(P|R)) --> (P|(Q-->R))";
+Goal "((P|Q)-->(P|R)) --> (P|(Q-->R))";
 by (safe_meson_tac 1);
 result();
 
 (*6*)
-goal HOL.thy "P | ~ P";
+Goal "P | ~ P";
 by (safe_meson_tac 1);
 result();
 
 (*7*)
-goal HOL.thy "P | ~ ~ ~ P";
+Goal "P | ~ ~ ~ P";
 by (safe_meson_tac 1);
 result();
 
 (*8.  Peirce's law*)
-goal HOL.thy "((P-->Q) --> P)  -->  P";
+Goal "((P-->Q) --> P)  -->  P";
 by (safe_meson_tac 1);
 result();
 
 (*9*)
-goal HOL.thy "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
+Goal "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
 by (safe_meson_tac 1);
 result();
 
 (*10*)
-goal HOL.thy "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)";
+Goal "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)";
 by (safe_meson_tac 1);
 result();
 
 (*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
-goal HOL.thy "P=(P::bool)";
+Goal "P=(P::bool)";
 by (safe_meson_tac 1);
 result();
 
 (*12.  "Dijkstra's law"*)
-goal HOL.thy "((P = Q) = R) = (P = (Q = R))";
+Goal "((P = Q) = R) = (P = (Q = R))";
 by (safe_meson_tac 1);
 result();
 
 (*13.  Distributive law*)
-goal HOL.thy "(P | (Q & R)) = ((P | Q) & (P | R))";
+Goal "(P | (Q & R)) = ((P | Q) & (P | R))";
 by (safe_meson_tac 1);
 result();
 
 (*14*)
-goal HOL.thy "(P = Q) = ((Q | ~P) & (~Q|P))";
+Goal "(P = Q) = ((Q | ~P) & (~Q|P))";
 by (safe_meson_tac 1);
 result();
 
 (*15*)
-goal HOL.thy "(P --> Q) = (~P | Q)";
+Goal "(P --> Q) = (~P | Q)";
 by (safe_meson_tac 1);
 result();
 
 (*16*)
-goal HOL.thy "(P-->Q) | (Q-->P)";
+Goal "(P-->Q) | (Q-->P)";
 by (safe_meson_tac 1);
 result();
 
 (*17*)
-goal HOL.thy "((P & (Q-->R))-->S)  =  ((~P | Q | S) & (~P | ~R | S))";
+Goal "((P & (Q-->R))-->S)  =  ((~P | Q | S) & (~P | ~R | S))";
 by (safe_meson_tac 1);
 result();
 
 writeln"Classical Logic: examples with quantifiers";
 
-goal HOL.thy "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))";
+Goal "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))";
 by (safe_meson_tac 1);
 result(); 
 
-goal HOL.thy "(? x. P --> Q x)  =  (P --> (? x. Q x))";
+Goal "(? x. P --> Q x)  =  (P --> (? x. Q x))";
 by (safe_meson_tac 1);
 result(); 
 
-goal HOL.thy "(? x. P x --> Q) = ((! x. P x) --> Q)";
+Goal "(? x. P x --> Q) = ((! x. P x) --> Q)";
 by (safe_meson_tac 1);
 result(); 
 
-goal HOL.thy "((! x. P x) | Q)  =  (! x. P x | Q)";
+Goal "((! x. P x) | Q)  =  (! x. P x | Q)";
 by (safe_meson_tac 1);
 result(); 
 
-goal HOL.thy "(! x. P x --> P(f x))  &  P d --> P(f(f(f d)))";
+Goal "(! x. P x --> P(f x))  &  P d --> P(f(f(f d)))";
 by (safe_meson_tac 1);
 result();
 
 (*Needs double instantiation of EXISTS*)
-goal HOL.thy "? x. P x --> P a & P b";
+Goal "? x. P x --> P a & P b";
 by (safe_meson_tac 1);
 result();
 
-goal HOL.thy "? z. P z --> (! x. P x)";
+Goal "? z. P z --> (! x. P x)";
 by (safe_meson_tac 1);
 result();
 
 writeln"Hard examples with quantifiers";
 
 writeln"Problem 18";
-goal HOL.thy "? y. ! x. P y --> P x";
+Goal "? y. ! x. P y --> P x";
 by (safe_meson_tac 1);
 result(); 
 
 writeln"Problem 19";
-goal HOL.thy "? x. ! y z. (P y --> Q z) --> (P x --> Q x)";
+Goal "? x. ! y z. (P y --> Q z) --> (P x --> Q x)";
 by (safe_meson_tac 1);
 result();
 
 writeln"Problem 20";
-goal HOL.thy "(! x y. ? z. ! w. (P x & Q y --> R z & S w))     \
+Goal "(! x y. ? z. ! w. (P x & Q y --> R z & S w))     \
 \   --> (? x y. P x & Q y) --> (? z. R z)";
 by (safe_meson_tac 1); 
 result();
 
 writeln"Problem 21";
-goal HOL.thy "(? x. P --> Q x) & (? x. Q x --> P) --> (? x. P=Q x)";
+Goal "(? x. P --> Q x) & (? x. Q x --> P) --> (? x. P=Q x)";
 by (safe_meson_tac 1); 
 result();
 
 writeln"Problem 22";
-goal HOL.thy "(! x. P = Q x)  -->  (P = (! x. Q x))";
+Goal "(! x. P = Q x)  -->  (P = (! x. Q x))";
 by (safe_meson_tac 1); 
 result();
 
 writeln"Problem 23";
-goal HOL.thy "(! x. P | Q x)  =  (P | (! x. Q x))";
+Goal "(! x. P | Q x)  =  (P | (! x. Q x))";
 by (safe_meson_tac 1);  
 result();
 
 writeln"Problem 24";  (*The first goal clause is useless*)
-goal HOL.thy "~(? x. S x & Q x) & (! x. P x --> Q x | R x) &  \
+Goal "~(? x. S x & Q x) & (! x. P x --> Q x | R x) &  \
 \    (~(? x. P x) --> (? x. Q x)) & (! x. Q x | R x --> S x)  \
 \   --> (? x. P x & R x)";
 by (safe_meson_tac 1); 
 result();
 
 writeln"Problem 25";
-goal HOL.thy "(? x. P x) &  \
+Goal "(? x. P x) &  \
 \       (! x. L x --> ~ (M x & R x)) &  \
 \       (! x. P x --> (M x & L x)) &   \
 \       ((! x. P x --> Q x) | (? x. P x & R x))  \
@@ -322,14 +324,14 @@
 result();
 
 writeln"Problem 26";  (*24 Horn clauses*)
-goal HOL.thy "((? x. p x) = (? x. q x)) &     \
+Goal "((? x. p x) = (? x. q x)) &     \
 \     (! x. ! y. p x & q y --> (r x = s y)) \
 \ --> ((! x. p x --> r x) = (! x. q x --> s x))";
 by (safe_meson_tac 1); 
 result();
 
 writeln"Problem 27";    (*13 Horn clauses*)
-goal HOL.thy "(? x. P x & ~Q x) &   \
+Goal "(? x. P x & ~Q x) &   \
 \             (! x. P x --> R x) &   \
 \             (! x. M x & L x --> P x) &   \
 \             ((? x. R x & ~ Q x) --> (! x. L x --> ~ R x))  \
@@ -338,7 +340,7 @@
 result();
 
 writeln"Problem 28.  AMENDED";  (*14 Horn clauses*)
-goal HOL.thy "(! x. P x --> (! x. Q x)) &   \
+Goal "(! x. P x --> (! x. Q x)) &   \
 \       ((! x. Q x | R x) --> (? x. Q x & S x)) &  \
 \       ((? x. S x) --> (! x. L x --> M x))  \
 \   --> (! x. P x & L x --> M x)";
@@ -347,21 +349,21 @@
 
 writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
         (*62 Horn clauses*)
-goal HOL.thy "(? x. F x) & (? y. G y)  \
+Goal "(? x. F x) & (? y. G y)  \
 \   --> ( ((! x. F x --> H x) & (! y. G y --> J y))  =   \
 \         (! x y. F x & G y --> H x & J y))";
 by (safe_meson_tac 1);          (*0.7 secs*)
 result();
 
 writeln"Problem 30";
-goal HOL.thy "(! x. P x | Q x --> ~ R x) & \
+Goal "(! x. P x | Q x --> ~ R x) & \
 \       (! x. (Q x --> ~ S x) --> P x & R x)  \
 \   --> (! x. S x)";
 by (safe_meson_tac 1);  
 result();
 
 writeln"Problem 31";  (*10 Horn clauses; first negative clauses is useless*)
-goal HOL.thy "~(? x. P x & (Q x | R x)) & \
+Goal "~(? x. P x & (Q x | R x)) & \
 \       (? x. L x & P x) & \
 \       (! x. ~ R x --> M x)  \
 \   --> (? x. L x & M x)";
@@ -369,7 +371,7 @@
 result();
 
 writeln"Problem 32";
-goal HOL.thy "(! x. P x & (Q x | R x)-->S x) & \
+Goal "(! x. P x & (Q x | R x)-->S x) & \
 \       (! x. S x & R x --> L x) & \
 \       (! x. M x --> R x)  \
 \   --> (! x. P x & M x --> L x)";
@@ -377,14 +379,14 @@
 result();
 
 writeln"Problem 33";  (*55 Horn clauses*)
-goal HOL.thy "(! x. P a & (P x --> P b)-->P c)  =    \
+Goal "(! x. P a & (P x --> P b)-->P c)  =    \
 \    (! x. (~P a | P x | P c) & (~P a | ~P b | P c))";
 by (safe_meson_tac 1);          (*5.6 secs*)
 result();
 
 writeln"Problem 34  AMENDED (TWICE!!)"; (*924 Horn clauses*)
 (*Andrews's challenge*)
-goal HOL.thy "((? x. ! y. p x = p y)  =               \
+Goal "((? x. ! y. p x = p y)  =               \
 \              ((? x. q x) = (! y. p y)))     =       \
 \             ((? x. ! y. q x = q y)  =               \
 \              ((? x. p x) = (! y. q y)))";
@@ -392,12 +394,12 @@
 result();
 
 writeln"Problem 35";
-goal HOL.thy "? x y. P x y -->  (! u v. P u v)";
+Goal "? x y. P x y -->  (! u v. P u v)";
 by (safe_meson_tac 1);
 result();
 
 writeln"Problem 36";  (*15 Horn clauses*)
-goal HOL.thy "(! x. ? y. J x y) & \
+Goal "(! x. ? y. J x y) & \
 \       (! x. ? y. G x y) & \
 \       (! x y. J x y | G x y -->       \
 \       (! z. J y z | G y z --> H x z))   \
@@ -406,7 +408,7 @@
 result();
 
 writeln"Problem 37";  (*10 Horn clauses*)
-goal HOL.thy "(! z. ? w. ! x. ? y. \
+Goal "(! z. ? w. ! x. ? y. \
 \          (P x z --> P y w) & P y z & (P y w --> (? u. Q u w))) & \
 \       (! x z. ~P x z --> (? y. Q y z)) & \
 \       ((? x y. Q x y) --> (! x. R x x))  \
@@ -415,7 +417,7 @@
 result();
 
 writeln"Problem 38";  (*Quite hard: 422 Horn clauses!!*)
-goal HOL.thy
+Goal
     "(! x. p a & (p x --> (? y. p y & r x y)) -->            \
 \          (? z. ? w. p z & r x w & r w z))  =                 \
 \    (! x. (~p a | p x | (? z. ? w. p z & r x w & r w z)) &  \
@@ -425,36 +427,36 @@
 result();
 
 writeln"Problem 39";
-goal HOL.thy "~ (? x. ! y. F y x = (~F y y))";
+Goal "~ (? x. ! y. F y x = (~F y y))";
 by (safe_meson_tac 1);
 result();
 
 writeln"Problem 40.  AMENDED";
-goal HOL.thy "(? y. ! x. F x y = F x x)  \
+Goal "(? y. ! x. F x y = F x x)  \
 \       -->  ~ (! x. ? y. ! z. F z y = (~F z x))";
 by (safe_meson_tac 1);
 result();
 
 writeln"Problem 41";
-goal HOL.thy "(! z. (? y. (! x. f x y = (f x z & ~ f x x))))    \
+Goal "(! z. (? y. (! x. f x y = (f x z & ~ f x x))))    \
 \              --> ~ (? z. ! x. f x z)";
 by (safe_meson_tac 1);
 result();
 
 writeln"Problem 42";
-goal HOL.thy "~ (? y. ! x. p x y = (~ (? z. p x z & p z x)))";
+Goal "~ (? y. ! x. p x y = (~ (? z. p x z & p z x)))";
 by (safe_meson_tac 1);
 result();
 
 writeln"Problem 43  NOW PROVED AUTOMATICALLY!!";
-goal HOL.thy "(! x. ! y. q x y = (! z. p z x = (p z y::bool)))  \
+Goal "(! x. ! y. q x y = (! z. p z x = (p z y::bool)))  \
 \         --> (! x. (! y. q x y = (q y x::bool)))";
 by (safe_best_meson_tac 1);     
 (*1.6 secs; iter. deepening is slightly slower*)
 result();
 
 writeln"Problem 44";  (*13 Horn clauses; 7-step proof*)
-goal HOL.thy "(! x. f x -->                                    \
+Goal "(! x. f x -->                                    \
 \             (? y. g y & h x y & (? y. g y & ~ h x y)))  &   \
 \             (? x. j x & (! y. g y --> h x y))               \
 \             --> (? x. j x & ~f x)";
@@ -462,7 +464,7 @@
 result();
 
 writeln"Problem 45";  (*27 Horn clauses; 54-step proof*)
-goal HOL.thy "(! x. f x & (! y. g y & h x y --> j x y)        \
+Goal "(! x. f x & (! y. g y & h x y --> j x y)        \
 \                     --> (! y. g y & h x y --> k y)) &       \
 \     ~ (? y. l y & k y) &                                    \
 \     (? x. f x & (! y. h x y --> l y)                        \
@@ -473,7 +475,7 @@
 result();
 
 writeln"Problem 46";  (*26 Horn clauses; 21-step proof*)
-goal HOL.thy
+Goal
     "(! x. f x & (! y. f y & h y x --> g y) --> g x) &      \
 \    ((? x. f x & ~g x) -->                                    \
 \     (? x. f x & ~g x & (! y. f y & ~g y --> j x y))) &    \
@@ -485,7 +487,7 @@
 
 writeln"Problem 47.  Schubert's Steamroller";
         (*26 clauses; 63 Horn clauses*)
-goal HOL.thy
+Goal
     "(! x. P1 x --> P0 x) & (? x. P1 x) &     \
 \    (! x. P2 x --> P0 x) & (? x. P2 x) &     \
 \    (! x. P3 x --> P0 x) & (? x. P3 x) &     \
@@ -507,7 +509,7 @@
 result();
 
 (*The Los problem?  Circulated by John Harrison*)
-goal HOL.thy "(! x y z. P x y & P y z --> P x z) &      \
+Goal "(! x y z. P x y & P y z --> P x z) &      \
 \      (! x y z. Q x y & Q y z --> Q x z) &             \
 \      (! x y. P x y --> P y x) &                       \
 \      (! x y. P x y | Q x y)                           \
@@ -516,7 +518,7 @@
 result();
 
 (*A similar example, suggested by Johannes Schumann and credited to Pelletier*)
-goal HOL.thy "(!x y z. P x y --> P y z --> P x z) --> \
+Goal "(!x y z. P x y --> P y z --> P x z) --> \
 \       (!x y z. Q x y --> Q y z --> Q x z) --> \
 \       (!x y. Q x y --> Q y x) -->  (!x y. P x y | Q x y) --> \
 \       (!x y. P x y) | (!x y. Q x y)";
@@ -525,7 +527,7 @@
 
 writeln"Problem 50";  
 (*What has this to do with equality?*)
-goal HOL.thy "(! x. P a x | (! y. P x y)) --> (? x. ! y. P x y)";
+Goal "(! x. P a x | (! y. P x y)) --> (? x. ! y. P x y)";
 by (safe_meson_tac 1);
 result();
 
@@ -533,7 +535,7 @@
 
 (*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
   meson_tac cannot report who killed Agatha. *)
-goal HOL.thy "lives agatha & lives butler & lives charles & \
+Goal "lives agatha & lives butler & lives charles & \
 \  (killed agatha agatha | killed butler agatha | killed charles agatha) & \
 \  (!x y. killed x y --> hates x y & ~richer x y) & \
 \  (!x. hates agatha x --> ~hates charles x) & \
@@ -546,7 +548,7 @@
 result();
 
 writeln"Problem 57";
-goal HOL.thy
+Goal
     "P (f a b) (f b c) & P (f b c) (f a c) & \
 \    (! x y z. P x y & P y z --> P x z)    -->   P (f a b) (f a c)";
 by (safe_meson_tac 1);
@@ -554,23 +556,23 @@
 
 writeln"Problem 58";
 (* Challenge found on info-hol *)
-goal HOL.thy
+Goal
     "! P Q R x. ? v w. ! y z. P x & Q y --> (P v | R w) & (R z --> Q v)";
 by (safe_meson_tac 1);
 result();
 
 writeln"Problem 59";
-goal HOL.thy "(! x. P x = (~P(f x))) --> (? x. P x & ~P(f x))";
+Goal "(! x. P x = (~P(f x))) --> (? x. P x & ~P(f x))";
 by (safe_meson_tac 1);
 result();
 
 writeln"Problem 60";
-goal HOL.thy "! x. P x (f x) = (? y. (! z. P z y --> P z (f x)) & P x y)";
+Goal "! x. P x (f x) = (? y. (! z. P z y --> P z (f x)) & P x y)";
 by (safe_meson_tac 1);
 result();
 
 writeln"Problem 62 as corrected in JAR 18 (1997), page 135";
-goal HOL.thy
+Goal
     "(ALL x. p a & (p x --> p(f x)) --> p(f(f x)))  =   \
 \    (ALL x. (~ p a | p x | p(f(f x))) &                        \
 \            (~ p a | ~ p(f x) | p(f(f x))))";
@@ -588,19 +590,19 @@
 fun axjoin ([],   q) = q
   | axjoin (p::ps, q) = "(" ^ p ^ ") --> (" ^ axjoin(ps,q) ^ ")";
 
-goal HOL.thy (axjoin([axa,axb,axd], "! x. T(i x x)"));
+Goal (axjoin([axa,axb,axd], "! x. T(i x x)"));
 by (safe_meson_tac 1);  
 result();
 
 writeln"Problem 66";  
-goal HOL.thy (axjoin([axa,axb,axc,axd], "! x. T(i x(n(n x)))"));
+Goal (axjoin([axa,axb,axc,axd], "! x. T(i x(n(n x)))"));
 (*TOO SLOW: more than 24 minutes!
 by (safe_meson_tac 1);
 result();
 *)
 
 writeln"Problem 67";  
-goal HOL.thy (axjoin([axa,axb,axc,axd], "! x. T(i(n(n x)) x)"));
+Goal (axjoin([axa,axb,axc,axd], "! x. T(i(n(n x)) x)"));
 (*TOO SLOW: more than 3 minutes!
 by (safe_meson_tac 1);
 result();