# HG changeset patch
# User wenzelm
# Date 1501601402 -7200
# Node ID 210dae34b8bc84ee95ec40e4ef0a51b7eec6b694
# Parent  fd89f97c80c22231442ffae02172379067a6c31c
misc tuning and modernization;

diff -r fd89f97c80c2 -r 210dae34b8bc src/HOL/ex/Classical.thy
--- a/src/HOL/ex/Classical.thy	Tue Aug 01 10:28:42 2017 +0200
+++ b/src/HOL/ex/Classical.thy	Tue Aug 01 17:30:02 2017 +0200
@@ -790,28 +790,32 @@
             (~ p a | ~ p(f x) | p(f(f x))))"
 by blast
 
-text\<open>* Charles Morgan's problems *\<close>
+text\<open>Charles Morgan's problems\<close>
+context
+  fixes T i n
+  assumes a: "\<forall>x y. T(i x(i y x))"
+    and b: "\<forall>x y z. T(i (i x (i y z)) (i (i x y) (i x z)))"
+    and c: "\<forall>x y. T(i (i (n x) (n y)) (i y x))"
+    and c': "\<forall>x y. T(i (i y x) (i (n x) (n y)))"
+    and d: "\<forall>x y. T(i x y) & T x --> T y"
+begin
 
-lemma
-  assumes a: "\<forall>x y.  T(i x(i y x))"
-      and b: "\<forall>x y z. T(i (i x (i y z)) (i (i x y) (i x z)))"
-      and c: "\<forall>x y.   T(i (i (n x) (n y)) (i y x))"
-      and c': "\<forall>x y.   T(i (i y x) (i (n x) (n y)))"
-      and d: "\<forall>x y.   T(i x y) & T x --> T y"
- shows True
-proof -
-  from a b d have "\<forall>x. T(i x x)" by blast
-  from a b c d have "\<forall>x. T(i x (n(n x)))" \<comment>\<open>Problem 66\<close>
-    by metis
-  from a b c d have "\<forall>x. T(i (n(n x)) x)" \<comment>\<open>Problem 67\<close>
-    by meson
-      \<comment>\<open>4.9s on griffon. 51061 inferences, depth 21\<close>
-  from a b c' d have "\<forall>x. T(i x (n(n x)))" 
-      \<comment>\<open>Problem 68: not proved.  Listed as satisfiable in TPTP (LCL078-1)\<close>
-oops
+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>
+  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>
+  using a b c' d oops
+
+end
 
 text\<open>Problem 71, as found in TPTP (SYN007+1.005)\<close>
 lemma "p1 = (p2 = (p3 = (p4 = (p5 = (p1 = (p2 = (p3 = (p4 = p5))))))))"
-by blast
+  by blast
 
 end