# HG changeset patch
# User wenzelm
# Date 1351966027 -3600
# Node ID e038198f7d080eab27cc67f9a870977ce79585e1
# Parent  7110422d4cb3f80ef8224d7d32f703d26c50d017
more concise/precise documentation;

diff -r 7110422d4cb3 -r e038198f7d08 src/Doc/Ref/document/classical.tex
--- a/src/Doc/Ref/document/classical.tex	Wed Nov 14 14:45:14 2012 +0100
+++ b/src/Doc/Ref/document/classical.tex	Sat Nov 03 19:07:07 2012 +0100
@@ -170,52 +170,6 @@
 resolution and also elim-resolution with the swapped form.
 \end{ttdescription}
 
-
-\section{Setting up the classical reasoner}\label{sec:classical-setup}
-\index{classical reasoner!setting up}
-Isabelle's classical object-logics, including \texttt{FOL} and \texttt{HOL}, 
-have the classical reasoner already set up.  
-When defining a new classical logic, you should set up the reasoner yourself.  
-It consists of the \ML{} functor \ttindex{ClassicalFun}, which takes the 
-argument signature \texttt{CLASSICAL_DATA}:
-\begin{ttbox} 
-signature CLASSICAL_DATA =
-  sig
-  val mp             : thm
-  val not_elim       : thm
-  val swap           : thm
-  val sizef          : thm -> int
-  val hyp_subst_tacs : (int -> tactic) list
-  end;
-\end{ttbox}
-Thus, the functor requires the following items:
-\begin{ttdescription}
-\item[\tdxbold{mp}] should be the Modus Ponens rule
-$\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$.
-
-\item[\tdxbold{not_elim}] should be the contradiction rule
-$\List{\neg\Var{P};\; \Var{P}} \Imp \Var{R}$.
-
-\item[\tdxbold{swap}] should be the swap rule
-$\List{\neg \Var{P}; \; \neg \Var{R}\Imp \Var{P}} \Imp \Var{R}$.
-
-\item[\ttindexbold{sizef}] is the heuristic function used for best-first
-search.  It should estimate the size of the remaining subgoals.  A good
-heuristic function is \ttindex{size_of_thm}, which measures the size of the
-proof state.  Another size function might ignore certain subgoals (say,
-those concerned with type-checking).  A heuristic function might simply
-count the subgoals.
-
-\item[\ttindexbold{hyp_subst_tacs}] is a list of tactics for substitution in
-the hypotheses, typically created by \ttindex{HypsubstFun} (see
-Chapter~\ref{substitution}).  This list can, of course, be empty.  The
-tactics are assumed to be safe!
-\end{ttdescription}
-The functor is not at all sensitive to the formalization of the
-object-logic.  It does not even examine the rules, but merely applies
-them according to its fixed strategy.  The functor resides in {\tt
-  Provers/classical.ML} in the Isabelle sources.
-
 \index{classical reasoner|)}
 
 %%% Local Variables: 
diff -r 7110422d4cb3 -r e038198f7d08 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Wed Nov 14 14:45:14 2012 +0100
+++ b/src/Provers/classical.ML	Sat Nov 03 19:07:07 2012 +0100
@@ -24,8 +24,9 @@
   val not_elim: thm  (* ~P ==> P ==> R *)
   val swap: thm  (* ~ P ==> (~ R ==> P) ==> R *)
   val classical: thm  (* (~ P ==> P) ==> P *)
-  val sizef: thm -> int  (* size function for BEST_FIRST *)
-  val hyp_subst_tacs: (int -> tactic) list
+  val sizef: thm -> int  (* size function for BEST_FIRST, typically size_of_thm *)
+  val hyp_subst_tacs: (int -> tactic) list (* optional tactics for substitution in
+    the hypotheses; assumed to be safe! *)
 end;
 
 signature BASIC_CLASSICAL =