# 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