--- a/doc-src/Ref/classical.tex Wed May 18 23:39:22 2011 +0200
+++ b/doc-src/Ref/classical.tex Fri May 20 14:03:42 2011 +0200
@@ -409,8 +409,7 @@
\section{The classical tactics}
\index{classical reasoner!tactics} If installed, the classical module provides
-powerful theorem-proving tactics. Most of them have capitalized analogues
-that use the default claset; see {\S}\ref{sec:current-claset}.
+powerful theorem-proving tactics.
\subsection{The tableau prover}
@@ -421,8 +420,6 @@
\begin{itemize}
\item It does not use the wrapper tacticals described above, such as
\ttindex{addss}.
-\item It ignores types, which can cause problems in HOL. If it applies a rule
- whose types are inappropriate, then proof reconstruction will fail.
\item It does not perform higher-order unification, as needed by the rule {\tt
rangeI} in HOL and \texttt{RepFunI} in ZF. There are often alternatives
to such rules, for example {\tt range_eqI} and \texttt{RepFun_eqI}.
@@ -479,12 +476,6 @@
completely. It tries to apply all fancy tactics it knows about,
performing a rather exhaustive search.
\end{ttdescription}
-They must be supplied both a simpset and a claset; therefore
-they are most easily called as \texttt{Auto_tac} and \texttt{Force_tac}, which
-use the default claset and simpset (see {\S}\ref{sec:current-claset} below).
-For interactive use,
-the shorthand \texttt{auto();} abbreviates \texttt{by Auto_tac;}
-while \texttt{force 1;} abbreviates \texttt{by (Force_tac 1);}
\subsection{Semi-automatic tactics}
@@ -601,73 +592,6 @@
\end{ttdescription}
-\subsection{The current claset}\label{sec:current-claset}
-
-Each theory is equipped with an implicit \emph{current claset}
-\index{claset!current}. This is a default set of classical
-rules. The underlying idea is quite similar to that of a current
-simpset described in {\S}\ref{sec:simp-for-dummies}; please read that
-section, including its warnings.
-
-The tactics
-\begin{ttbox}
-Blast_tac : int -> tactic
-Auto_tac : tactic
-Force_tac : int -> tactic
-Fast_tac : int -> tactic
-Best_tac : int -> tactic
-Deepen_tac : int -> int -> tactic
-Clarify_tac : int -> tactic
-Clarify_step_tac : int -> tactic
-Clarsimp_tac : int -> tactic
-Safe_tac : tactic
-Safe_step_tac : int -> tactic
-Step_tac : int -> tactic
-\end{ttbox}
-\indexbold{*Blast_tac}\indexbold{*Auto_tac}\indexbold{*Force_tac}
-\indexbold{*Best_tac}\indexbold{*Fast_tac}%
-\indexbold{*Deepen_tac}
-\indexbold{*Clarify_tac}\indexbold{*Clarify_step_tac}\indexbold{*Clarsimp_tac}
-\indexbold{*Safe_tac}\indexbold{*Safe_step_tac}
-\indexbold{*Step_tac}
-make use of the current claset. For example, \texttt{Blast_tac} is defined as
-\begin{ttbox}
-fun Blast_tac i st = blast_tac (claset()) i st;
-\end{ttbox}
-and gets the current claset, only after it is applied to a proof state.
-The functions
-\begin{ttbox}
-AddSIs, AddSEs, AddSDs, AddIs, AddEs, AddDs: thm list -> unit
-\end{ttbox}
-\indexbold{*AddSIs} \indexbold{*AddSEs} \indexbold{*AddSDs}
-\indexbold{*AddIs} \indexbold{*AddEs} \indexbold{*AddDs}
-are used to add rules to the current claset. They work exactly like their
-lower case counterparts, such as \texttt{addSIs}. Calling
-\begin{ttbox}
-Delrules : thm list -> unit
-\end{ttbox}
-deletes rules from the current claset.
-
-
-\subsection{Accessing the current claset}
-\label{sec:access-current-claset}
-
-the functions to access the current claset are analogous to the functions
-for the current simpset, so please see \ref{sec:access-current-simpset}
-for a description.
-\begin{ttbox}
-claset : unit -> claset
-claset_ref : unit -> claset ref
-claset_of : theory -> claset
-claset_ref_of : theory -> claset ref
-print_claset : theory -> unit
-CLASET :(claset -> tactic) -> tactic
-CLASET' :(claset -> 'a -> tactic) -> 'a -> tactic
-CLASIMPSET :(clasimpset -> tactic) -> tactic
-CLASIMPSET' :(clasimpset -> 'a -> tactic) -> 'a -> tactic
-\end{ttbox}
-
-
\subsection{Other useful tactics}
\index{tactics!for contradiction}
\index{tactics!for Modus Ponens}
@@ -766,20 +690,6 @@
\index{classical reasoner|)}
-\section{Setting up the combination with the simplifier}
-\label{sec:clasimp-setup}
-
-To combine the classical reasoner and the simplifier, we simply call the
-\ML{} functor \ttindex{ClasimpFun} that assembles the parts as required.
-It takes a structure (of signature \texttt{CLASIMP_DATA}) as
-argment, which can be contructed on the fly:
-\begin{ttbox}
-structure Clasimp = ClasimpFun
- (structure Simplifier = Simplifier
- and Classical = Classical
- and Blast = Blast);
-\end{ttbox}
-%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "ref"
--- a/doc-src/Ref/defining.tex Wed May 18 23:39:22 2011 +0200
+++ b/doc-src/Ref/defining.tex Fri May 20 14:03:42 2011 +0200
@@ -249,8 +249,7 @@
conceptually just concatenated from left to right, with the standard
syntax output table always coming last as default. Thus mixfix
productions of preceding modes in the list may override those of later
-ones. Also note that token translations are always relative to some
-print mode (see \S\ref{sec:tok_tr}).
+ones.
\medskip The canonical application of print modes is optional printing
of mathematical symbols from a special screen font instead of {\sc
--- a/doc-src/Ref/simplifier.tex Wed May 18 23:39:22 2011 +0200
+++ b/doc-src/Ref/simplifier.tex Fri May 20 14:03:42 2011 +0200
@@ -269,59 +269,6 @@
\end{ttdescription}
-\subsection{Accessing the current simpset}
-\label{sec:access-current-simpset}
-
-\begin{ttbox}
-simpset : unit -> simpset
-simpset_ref : unit -> simpset ref
-simpset_of : theory -> simpset
-simpset_ref_of : theory -> simpset ref
-print_simpset : theory -> unit
-SIMPSET :(simpset -> tactic) -> tactic
-SIMPSET' :(simpset -> 'a -> tactic) -> 'a -> tactic
-\end{ttbox}
-
-Each theory contains a current simpset\index{simpset!current} stored
-within a private ML reference variable. This can be retrieved and
-modified as follows.
-
-\begin{ttdescription}
-
-\item[\ttindexbold{simpset}();] retrieves the simpset value from the
- current theory context.
-
-\item[\ttindexbold{simpset_ref}();] retrieves the simpset reference
- variable from the current theory context. This can be assigned to
- by using \texttt{:=} in ML.
-
-\item[\ttindexbold{simpset_of} $thy$;] retrieves the simpset value
- from theory $thy$.
-
-\item[\ttindexbold{simpset_ref_of} $thy$;] retrieves the simpset
- reference variable from theory $thy$.
-
-\item[\ttindexbold{print_simpset} $thy$;] prints the current simpset
- of theory $thy$ in the same way as \texttt{print_ss}.
-
-\item[\ttindexbold{SIMPSET} $tacf$, \ttindexbold{SIMPSET'} $tacf'$]
- are tacticals that make a tactic depend on the implicit current
- simpset of the theory associated with the proof state they are
- applied on.
-
-\end{ttdescription}
-
-\begin{warn}
- There is a small difference between \texttt{(SIMPSET'~$tacf$)} and
- \texttt{($tacf\,$(simpset()))}. For example \texttt{(SIMPSET'
- simp_tac)} would depend on the theory of the proof state it is
- applied to, while \texttt{(simp_tac (simpset()))} implicitly refers
- to the current theory context. Both are usually the same in proof
- scripts, provided that goals are only stated within the current
- theory. Robust programs would not count on that, of course.
-\end{warn}
-
-
\subsection{Rewrite rules}
\begin{ttbox}
addsimps : simpset * thm list -> simpset \hfill{\bf infix 4}
@@ -1262,36 +1209,6 @@
effect for conjunctions.
-\subsection{Splitter setup}\index{simplification!setting up the splitter}
-
-To set up case splitting, we have to call the \ML{} functor \ttindex{
-SplitterFun}, which takes the argument signature \texttt{SPLITTER_DATA}.
-So we prove the theorem \texttt{meta_eq_to_iff} below and store it, together
-with the \texttt{mk_eq} function described above and several standard
-theorems, in the structure \texttt{SplitterData}. Calling the functor with
-this data yields a new instantiation of the splitter for our logic.
-\begin{ttbox}
-val meta_eq_to_iff = prove_goal IFOL.thy "x==y ==> x<->y"
- (fn [prem] => [rewtac prem, rtac iffI 1, atac 1, atac 1]);
-\ttbreak
-structure SplitterData =
- struct
- structure Simplifier = Simplifier
- val mk_eq = mk_eq
- val meta_eq_to_iff = meta_eq_to_iff
- val iffD = iffD2
- val disjE = disjE
- val conjE = conjE
- val exE = exE
- val contrapos = contrapos
- val contrapos2 = contrapos2
- val notnotD = notnotD
- end;
-\ttbreak
-structure Splitter = SplitterFun(SplitterData);
-\end{ttbox}
-
-
\index{simplification|)}
--- a/doc-src/Ref/syntax.tex Wed May 18 23:39:22 2011 +0200
+++ b/doc-src/Ref/syntax.tex Fri May 20 14:03:42 2011 +0200
@@ -43,7 +43,7 @@
\AST{} & \\
$\downarrow$ & \AST{} rewriting (macros) \\
\AST{} & \\
-$\downarrow$ & print \AST{} translation, token translation \\
+$\downarrow$ & print \AST{} translation \\
string &
\end{tabular}
@@ -564,9 +564,6 @@
This example demonstrates the use of recursive macros to implement a
convenient notation for finite sets.
-\index{*empty constant}\index{*insert constant}\index{{}@\verb'{}' symbol}
-\index{"@Enum@{\tt\at Enum} constant}
-\index{"@Finset@{\tt\at Finset} constant}
\begin{ttbox}
FinSyntax = SetSyntax +
types
@@ -602,7 +599,6 @@
had needed polymorphic enumerations, we could have used the predefined
nonterminal symbol \ndx{args} and skipped this part altogether.
-\index{"@Finset@{\tt\at Finset} constant}
Next follows {\tt empty}, which is already equipped with its syntax
\verb|{}|, and {\tt insert} without concrete syntax. The syntactic
constant {\tt\at Finset} provides concrete syntax for enumerations of~{\tt
@@ -850,53 +846,6 @@
style. \index{translations|)} \index{syntax!transformations|)}
-\section{Token translations} \label{sec:tok_tr}
-\index{token translations|(}
-%
-Isabelle's meta-logic features quite a lot of different kinds of
-identifiers, namely {\em class}, {\em tfree}, {\em tvar}, {\em free},
-{\em bound}, {\em var}. One might want to have these printed in
-different styles, e.g.\ in bold or italic, or even transcribed into
-something more readable like $\alpha, \alpha', \beta$ instead of {\tt
- 'a}, {\tt 'aa}, {\tt 'b} for type variables. Token translations
-provide a means to such ends, enabling the user to install certain
-\ML{} functions associated with any logical \rmindex{token class} and
-depending on some \rmindex{print mode}.
-
-The logical class of identifiers can not necessarily be determined by
-its syntactic category, though. For example, consider free vs.\ bound
-variables. So Isabelle's pretty printing mechanism, starting from
-fully typed terms, has to be careful to preserve this additional
-information\footnote{This is done by marking atoms in abstract syntax
- trees appropriately. The marks are actually visible by print
- translation functions -- they are just special constants applied to
- atomic asts, for example \texttt{("_bound" x)}.}. In particular,
-user-supplied print translation functions operating on terms have to
-be well-behaved in this respect. Free identifiers introduced to
-represent bound variables have to be marked appropriately (cf.\ the
-example at the end of \S\ref{sec:tr_funs}).
-
-\medskip Token translations may be installed by declaring the
-\ttindex{token_translation} value within the \texttt{ML} section of a theory
-definition file:
-\begin{ttbox}
-val token_translation:
- (string * string * (string -> string * real)) list
-\end{ttbox}
-The elements of this list are of the form $(m, c, f)$, where $m$ is a print
-mode identifier, $c$ a token class, and $f\colon string \to string \times
-real$ the actual translation function. Assuming that $x$ is of identifier
-class $c$, and print mode $m$ is the first (active) mode providing some
-translation for $c$, then $x$ is output according to $f(x) = (x', len)$.
-Thereby $x'$ is the modified identifier name and $len$ its visual length in
-terms of characters (e.g.\ length 1.0 would correspond to $1/2$\,em in
-\LaTeX). Thus $x'$ may include non-printing parts like control sequences or
-markup information for typesetting systems.
-
-
-\index{token translations|)}
-
-
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "ref"
--- a/doc-src/Ref/theories.tex Wed May 18 23:39:22 2011 +0200
+++ b/doc-src/Ref/theories.tex Fri May 20 14:03:42 2011 +0200
@@ -2,52 +2,6 @@
\chapter{Theories, Terms and Types} \label{theories}
\index{theories|(}
-\section{The theory loader}\label{sec:more-theories}
-\index{theories!reading}\index{files!reading}
-
-Isabelle's theory loader manages dependencies of the internal graph of theory
-nodes (the \emph{theory database}) and the external view of the file system.
-
-\medskip Theory and {\ML} files are located by skimming through the
-directories listed in Isabelle's internal load path, which merely contains the
-current directory ``\texttt{.}'' by default. The load path may be accessed by
-the following operations.
-
-\begin{ttbox}
-show_path: unit -> string list
-add_path: string -> unit
-del_path: string -> unit
-reset_path: unit -> unit
-with_path: string -> ('a -> 'b) -> 'a -> 'b
-no_document: ('a -> 'b) -> 'a -> 'b
-\end{ttbox}
-
-\begin{ttdescription}
-\item[\ttindexbold{show_path}();] displays the load path components in
- canonical string representation (which is always according to Unix rules).
-
-\item[\ttindexbold{add_path} "$dir$";] adds component $dir$ to the beginning
- of the load path.
-
-\item[\ttindexbold{del_path} "$dir$";] removes any occurrences of component
- $dir$ from the load path.
-
-\item[\ttindexbold{reset_path}();] resets the load path to ``\texttt{.}''
- (current directory) only.
-
-\item[\ttindexbold{with_path} "$dir$" $f$ $x$;] temporarily adds component
- $dir$ to the beginning of the load path while executing $(f~x)$.
-
-\item[\ttindexbold{no_document} $f$ $x$;] temporarily disables {\LaTeX}
- document generation while executing $(f~x)$.
-
-\end{ttdescription}
-
-Furthermore, in operations referring indirectly to some file (e.g.\
-\texttt{use_dir}) the argument may be prefixed by a directory that will be
-temporarily appended to the load path, too.
-
-
\section{Basic operations on theories}\label{BasicOperationsOnTheories}
\subsection{*Theory inclusion}