ex/mesontest.ML

 by (depth_prolog_tac horns26);	(*6 secs*)
 
 
 
 writeln"Problem 43  NOW PROVED AUTOMATICALLY!!";
-goal HOL.thy "(! x. ! y. q(x,y) = (! z. p(z,x) = p(z,y)::bool))	\
-\         --> (! x. (! y. q(x,y) = q(y,x)::bool))";
+goal HOL.thy "(! 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;
 val nnf43 = make_nnf prem43;
 val xsko43 = skolemize nnf43;
 by (cut_facts_tac [xsko43] 1 THEN REPEAT (etac exE 1));

 goal HOL.thy "(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 HOL.thy "P=(P::bool)";
 by (safe_meson_tac 1);
 result();
 
 (*12.  "Dijkstra's law"*)
 goal HOL.thy "((P = Q) = R) = (P = (Q = R))";

 goal HOL.thy "~ (? 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))	\
-\         --> (! x. (! y. q(x,y) = q(y,x)::bool))";
+goal HOL.thy "(! x. ! y. q(x,y) = (! z. p(z,x) = (p(z,y)::bool)))	\
+\         --> (! x. (! y. q(x,y) = (q(y,x)::bool)))";
 by (safe_meson_tac 1);
 result();
 
 writeln"Problem 44";
 goal HOL.thy "(! x. f(x) -->					\