doc-src/HOL/HOL.tex

 like all other Isabelle theories, uses meta-equality~({\tt==}) for
 definitions.
 \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}
 mentions the type variable~{\tt'a}.  This allows you to instantiate
 type variables explicitly by calling \texttt{res_inst_tac}.

 
 There is also a large collection of monotonicity theorems for constructions
 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
 simplification set for higher-order logic is~\ttindexbold{HOL_ss};
 even more frugal is \ttindexbold{HOL_basic_ss}.  Equality~($=$), which

 
 HOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for an
 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
 containing a subterm of the form \texttt{if}~$b$~{\tt then\dots else\dots}
 often require a case distinction on $b$. This is expressed by the theorem

 \begin{ttbox}
 \ttindexbold{Addsplits}: thm list -> unit
 \ttindexbold{Delsplits}: thm list -> unit
 \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$,
 $\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for introducing new