# HG changeset patch
# User wenzelm
# Date 1218653838 -7200
# Node ID c749054238951d9f8d396c2a7559f9d9b9a87074
# Parent  eda38d6e55da387bea04d8cfaabdd298e447ba7d
tuned document;

diff -r eda38d6e55da -r c74905423895 src/FOL/FOL.thy
--- 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
diff -r eda38d6e55da -r c74905423895 src/FOL/cladata.ML
--- 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