--- a/doc-src/HOL/HOL.tex Thu Jun 02 14:11:24 2011 +0200
+++ b/doc-src/HOL/HOL.tex Fri Jun 03 21:32:48 2011 +0200
@@ -310,8 +310,7 @@
\begin{warn}
The definitions above should never be expanded and are shown for completeness
only. Instead users should reason in terms of the derived rules shown below
-or, better still, using high-level tactics
-(see~{\S}\ref{sec:HOL:generic-packages}).
+or, better still, using high-level tactics.
\end{warn}
Some of the rules mention type variables; for example, \texttt{refl}
@@ -880,13 +879,7 @@
on sets in the file \texttt{HOL/mono.ML}.
-\section{Generic packages}
-\label{sec:HOL:generic-packages}
-
-HOL instantiates most of Isabelle's generic packages, making available the
-simplifier and the classical reasoner.
-
-\subsection{Simplification and substitution}
+\section{Simplification and substitution}
Simplification tactics tactics such as \texttt{Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset
(\texttt{simpset()}), which works for most purposes. A quite minimal
@@ -932,7 +925,7 @@
equality throughout a subgoal and its hypotheses. This tactic uses HOL's
general substitution rule.
-\subsubsection{Case splitting}
+\subsection{Case splitting}
\label{subsec:HOL:case:splitting}
HOL also provides convenient means for case splitting during rewriting. Goals
@@ -989,115 +982,6 @@
\end{ttbox}
for adding splitting rules to, and deleting them from the current simpset.
-\subsection{Classical reasoning}
-
-HOL derives classical introduction rules for $\disj$ and~$\exists$, as well as
-classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule; recall
-Fig.\ts\ref{hol-lemmas2} above.
-
-The classical reasoner is installed. Tactics such as \texttt{Blast_tac} and
-{\tt Best_tac} refer to the default claset (\texttt{claset()}), which works
-for most purposes. Named clasets include \ttindexbold{prop_cs}, which
-includes the propositional rules, and \ttindexbold{HOL_cs}, which also
-includes quantifier rules. See the file \texttt{HOL/cladata.ML} for lists of
-the classical rules,
-and \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
-{Chap.\ts\ref{chap:classical}} for more discussion of classical proof methods.
-
-
-%FIXME outdated, both from the Isabelle and SVC perspective
-% \section{Calling the decision procedure SVC}\label{sec:HOL:SVC}
-
-% \index{SVC decision procedure|(}
-
-% The Stanford Validity Checker (SVC) is a tool that can check the validity of
-% certain types of formulae. If it is installed on your machine, then
-% Isabelle/HOL can be configured to call it through the tactic
-% \ttindex{svc_tac}. It is ideal for large tautologies and complex problems in
-% linear arithmetic. Subexpressions that SVC cannot handle are automatically
-% replaced by variables, so you can call the tactic on any subgoal. See the
-% file \texttt{HOL/ex/svc_test.ML} for examples.
-% \begin{ttbox}
-% svc_tac : int -> tactic
-% Svc.trace : bool ref \hfill{\bf initially false}
-% \end{ttbox}
-
-% \begin{ttdescription}
-% \item[\ttindexbold{svc_tac} $i$] attempts to prove subgoal~$i$ by translating
-% it into a formula recognized by~SVC\@. If it succeeds then the subgoal is
-% removed. It fails if SVC is unable to prove the subgoal. It crashes with
-% an error message if SVC appears not to be installed. Numeric variables may
-% have types \texttt{nat}, \texttt{int} or \texttt{real}.
-
-% \item[\ttindexbold{Svc.trace}] is a flag that, if set, causes \texttt{svc_tac}
-% to trace its operations: abstraction of the subgoal, translation to SVC
-% syntax, SVC's response.
-% \end{ttdescription}
-
-% Here is an example, with tracing turned on:
-% \begin{ttbox}
-% set Svc.trace;
-% {\out val it : bool = true}
-% Goal "(#3::nat)*a <= #2 + #4*b + #6*c & #11 <= #2*a + b + #2*c & \ttback
-% \ttback a + #3*b <= #5 + #2*c --> #2 + #3*b <= #2*a + #6*c";
-
-% by (svc_tac 1);
-% {\out Subgoal abstracted to}
-% {\out #3 * a <= #2 + #4 * b + #6 * c &}
-% {\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c -->}
-% {\out #2 + #3 * b <= #2 * a + #6 * c}
-% {\out Calling SVC:}
-% {\out (=> (<= 0 (F_c) ) (=> (<= 0 (F_b) ) (=> (<= 0 (F_a) )}
-% {\out (=> (AND (<= {* 3 (F_a) } {+ {+ 2 {* 4 (F_b) } } }
-% {\out {* 6 (F_c) } } ) (AND (<= 11 {+ {+ {* 2 (F_a) } (F_b) }}
-% {\out {* 2 (F_c) } } ) (<= {+ (F_a) {* 3 (F_b) } } {+ 5 }
-% {\out {* 2 (F_c) } } ) ) ) (< {+ 2 {* 3 (F_b) } } {+ 1 {+ }
-% {\out {* 2 (F_a) } {* 6 (F_c) } } } ) ) ) ) ) }
-% {\out SVC Returns:}
-% {\out VALID}
-% {\out Level 1}
-% {\out #3 * a <= #2 + #4 * b + #6 * c &}
-% {\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c -->}
-% {\out #2 + #3 * b <= #2 * a + #6 * c}
-% {\out No subgoals!}
-% \end{ttbox}
-
-
-% \begin{warn}
-% Calling \ttindex{svc_tac} entails an above-average risk of
-% unsoundness. Isabelle does not check SVC's result independently. Moreover,
-% the tactic translates the submitted formula using code that lies outside
-% Isabelle's inference core. Theorems that depend upon results proved using SVC
-% (and other oracles) are displayed with the annotation \texttt{[!]} attached.
-% You can also use \texttt{\#der (rep_thm $th$)} to examine the proof object of
-% theorem~$th$, as described in the \emph{Reference Manual}.
-% \end{warn}
-
-% To start, first download SVC from the Internet at URL
-% \begin{ttbox}
-% http://agamemnon.stanford.edu/~levitt/vc/index.html
-% \end{ttbox}
-% and install it using the instructions supplied. SVC requires two environment
-% variables:
-% \begin{ttdescription}
-% \item[\ttindexbold{SVC_HOME}] is an absolute pathname to the SVC
-% distribution directory.
-
-% \item[\ttindexbold{SVC_MACHINE}] identifies the type of computer and
-% operating system.
-% \end{ttdescription}
-% You can set these environment variables either using the Unix shell or through
-% an Isabelle \texttt{settings} file. Isabelle assumes SVC to be installed if
-% \texttt{SVC_HOME} is defined.
-
-% \paragraph*{Acknowledgement.} This interface uses code supplied by S{\o}ren
-% Heilmann.
-
-
-% \index{SVC decision procedure|)}
-
-
-
\section{Types}\label{sec:HOL:Types}
This section describes HOL's basic predefined types ($\alpha \times \beta$,