--- a/src/FOL/FOL.thy Wed Aug 13 20:57:16 2008 +0200
+++ b/src/FOL/FOL.thy Wed Aug 13 20:57:18 2008 +0200
@@ -164,6 +164,9 @@
lemma swap: "~ P ==> (~ R ==> P) ==> R"
by (rule classical) iprover
+
+section {* Classical Reasoner *}
+
use "cladata.ML"
setup Cla.setup
setup cla_setup
--- a/src/FOL/cladata.ML Wed Aug 13 20:57:16 2008 +0200
+++ b/src/FOL/cladata.ML Wed Aug 13 20:57:18 2008 +0200
@@ -6,8 +6,6 @@
Setting up the classical reasoner.
*)
-section "Classical Reasoner";
-
(*** Applying ClassicalFun to create a classical prover ***)
structure Classical_Data =
struct