src/HOL/ex/Classical.thy

 JAR 29: 3-4 (2002), pages 253-275\<close>
 lemma "(\<forall>x y z. R(x,y) & R(y,z) --> R(x,z)) &
        (\<forall>x. \<exists>y. R(x,y)) -->
        ~ (\<forall>x. P x = (\<forall>y. R(x,y) --> ~ P y))"
 by (tactic\<open>Meson.safe_best_meson_tac @{context} 1\<close>)
-    \<comment>\<open>In contrast, \<open>meson\<close> is SLOW: 7.6s on griffon\<close>
+    \<comment> \<open>In contrast, \<open>meson\<close> is SLOW: 7.6s on griffon\<close>
 
 
 subsubsection\<open>Pelletier's examples\<close>
 text\<open>1\<close>
 lemma "(P --> Q)  =  (~Q --> ~P)"

 lemma "(\<forall>z. \<exists>w. \<forall>x. \<exists>y.
            (P x z --> P y w) & P y z & (P y w --> (\<exists>u. Q u w))) &
       (\<forall>x z. ~P x z --> (\<exists>y. Q y z)) &
       ((\<exists>x y. Q x y) --> (\<forall>x. R x x))
     --> (\<forall>x. \<exists>y. R x y)"
-by blast \<comment>\<open>causes unification tracing messages\<close>
+by blast \<comment> \<open>causes unification tracing messages\<close>
 
 
 text\<open>Problem 38\<close>  text\<open>Quite hard: 422 Horn clauses!!\<close>
 lemma "(\<forall>x. p a & (p x --> (\<exists>y. p y & r x y)) -->
            (\<exists>z. \<exists>w. p z & r x w & r w z))  =

        (\<forall>x y. bird x & caterpillar y \<longrightarrow> eats x y) &
        (\<forall>x y. bird x & snail y \<longrightarrow> ~eats x y) &
        (\<forall>x. (caterpillar x \<or> snail x) \<longrightarrow> (\<exists>y. plant y & eats x y))
        \<longrightarrow> (\<exists>x y. animal x & animal y & (\<exists>z. grain z & eats y z & eats x y))"
 by (tactic\<open>Meson.safe_best_meson_tac @{context} 1\<close>)
-    \<comment>\<open>Nearly twice as fast as \<open>meson\<close>,
+    \<comment> \<open>Nearly twice as fast as \<open>meson\<close>,
         which performs iterative deepening rather than best-first search\<close>
 
 text\<open>The Los problem. Circulated by John Harrison\<close>
 lemma "(\<forall>x y z. P x y & P y z --> P x z) &
        (\<forall>x y z. Q x y & Q y z --> Q x z) &

 begin
 
 lemma "\<forall>x. T(i x x)"
   using a b d by blast
 
-lemma "\<forall>x. T(i x (n(n x)))" \<comment>\<open>Problem 66\<close>
+lemma "\<forall>x. T(i x (n(n x)))" \<comment> \<open>Problem 66\<close>
   using a b c d by metis
 
-lemma "\<forall>x. T(i (n(n x)) x)" \<comment>\<open>Problem 67\<close>
-  using a b c d by meson \<comment>\<open>4.9s on griffon. 51061 inferences, depth 21\<close>
-
-lemma "\<forall>x. T(i x (n(n x)))" \<comment>\<open>Problem 68: not proved.  Listed as satisfiable in TPTP (LCL078-1)\<close>
+lemma "\<forall>x. T(i (n(n x)) x)" \<comment> \<open>Problem 67\<close>
+  using a b c d by meson \<comment> \<open>4.9s on griffon. 51061 inferences, depth 21\<close>
+
+lemma "\<forall>x. T(i x (n(n x)))" \<comment> \<open>Problem 68: not proved.  Listed as satisfiable in TPTP (LCL078-1)\<close>
   using a b c' d oops
 
 end
 
 text\<open>Problem 71, as found in TPTP (SYN007+1.005)\<close>