--- a/doc-src/Ref/classical.tex Thu Feb 05 10:26:16 1998 +0100
+++ b/doc-src/Ref/classical.tex Thu Feb 05 10:26:59 1998 +0100
@@ -339,9 +339,12 @@
\index{simplification!from classical reasoner} The wrapper tacticals
underly the operator addss, which combines each search step by
simplification. Strictly speaking, \texttt{addss} is not part of the
-classical reasoner. It should be defined (using \texttt{addSaltern
- (CHANGED o (safe_asm_more_full_simp_tac ss)}) when the simplifier is
-installed.
+classical reasoner. It should be defined when the simplifier is
+installed:
+\begin{ttbox}
+infix 4 addss;
+fun cs addss ss = cs addbefore asm_full_simp_tac ss;
+\end{ttbox}
\begin{ttdescription}
\item[$cs$ addss $ss$] \indexbold{*addss}
@@ -396,7 +399,7 @@
instantiating quantifiers yourself.
\begin{ttdescription}
\item[\ttindexbold{clarify_tac} $cs$ $i$] performs a series of safe steps on
-subgoal~$i$, using \texttt{clarify_step_tac}.
+subgoal~$i$ by repeatedly calling \texttt{clarify_step_tac}.
\item[\ttindexbold{clarify_step_tac} $cs$ $i$] performs a safe step on
subgoal~$i$. No splitting step is applied; for example, the subgoal $A\conj
--- a/doc-src/Ref/defining.tex Thu Feb 05 10:26:16 1998 +0100
+++ b/doc-src/Ref/defining.tex Thu Feb 05 10:26:59 1998 +0100
@@ -85,7 +85,7 @@
\index{priority grammars|)}
-\begin{figure}
+\begin{figure}\small
\begin{center}
\begin{tabular}{rclc}
$any$ &=& $prop$ ~~$|$~~ $logic$ \\\\
@@ -376,7 +376,7 @@
syntax trees. Section \S\ref{sec:asts} below discusses this obscure
matter.\index{constants!for translations}
- \item[{\tt parse_translation}, {\tt print_translation}] list sets
+ \item[{\tt parse_translation}, {\tt print_translation}] list the sets
of constants that invoke translation functions for terms (see
\S\ref{sec:tr_funs}).
\end{description}
--- a/doc-src/Ref/ref.ind Thu Feb 05 10:26:16 1998 +0100
+++ b/doc-src/Ref/ref.ind Thu Feb 05 10:26:59 1998 +0100
@@ -217,12 +217,15 @@
\item {\tt Deriv.size}, \bold{49}
\item {\tt Deriv.tree}, \bold{49}
\item {\tt dest_eq}, \bold{101}
+ \item {\tt dest_imp}, \bold{101}
\item {\tt dest_state}, \bold{41}
+ \item {\tt dest_Trueprop}, \bold{101}
\item destruct-resolution, 18
\item {\tt DETERM}, \bold{33}
\item discrimination nets, \bold{25}
\item {\tt distinct_subgoals_tac}, \bold{23}
\item {\tt dmatch_tac}, \bold{18}
+ \item {\tt domain_type}, \bold{102}
\item {\tt dres_inst_tac}, \bold{19}
\item {\tt dresolve_tac}, \bold{18}
\item {\tt dtac}, \bold{20}
@@ -240,7 +243,7 @@
\item {\tt eq_assume_tac}, \bold{18}, 131
\item {\tt eq_assumption}, \bold{47}
\item {\tt eq_mp_tac}, \bold{138}
- \item {\tt eq_reflection} theorem, \bold{101}, 122
+ \item {\tt eq_reflection} theorem, \bold{102}, 122
\item {\tt eq_thm}, \bold{33}
\item {\tt eq_thy}, \bold{58}
\item {\tt equal_elim}, \bold{44}
@@ -347,7 +350,7 @@
\item {\tt IF_UNSOLVED}, \bold{33}
\item {\tt iff_reflection} theorem, 122
\item {\tt IFOL_ss}, \bold{125}
- \item {\tt imp_intr} theorem, \bold{101}
+ \item {\tt imp_intr} theorem, \bold{102}
\item {\tt implies_elim}, \bold{44}
\item {\tt implies_elim_list}, \bold{44}
\item {\tt implies_intr}, \bold{44}
@@ -395,7 +398,7 @@
\item macros, 88--94
\item {\tt make_elim}, \bold{40}, 132
- \item {\tt Match} exception, 96, 101
+ \item {\tt Match} exception, 95
\item {\tt match_tac}, \bold{18}, 131
\item {\tt max_pri}, 68, \bold{74}
\item {\tt merge_ss}, \bold{106}
@@ -451,9 +454,7 @@
\subitem renaming, 13, 22, 48
\item {\tt parents_of}, \bold{59}
\item parse trees, 83
- \item {\tt parse_ast_translation}, 95
\item {\tt parse_rules}, 90
- \item {\tt parse_translation}, 95
\item pattern, higher-order, \bold{108}
\item {\tt pause_tac}, \bold{27}
\item Poly/{\ML} compiler, 5
@@ -470,7 +471,6 @@
\item {\tt prin}, 6, \bold{15}
\item print mode, 52, 97
\item print modes, 78--79
- \item {\tt print_ast_translation}, 95
\item {\tt print_cs}, \bold{131}
\item {\tt print_data}, \bold{59}
\item {\tt print_depth}, \bold{4}
@@ -485,7 +485,6 @@
\item {\tt print_tac}, \bold{27}
\item {\tt print_theory}, \bold{59}
\item {\tt print_thm}, \bold{38}
- \item {\tt print_translation}, 95
\item printing control, 3--5
\item {\tt printyp}, \bold{15}
\item priorities, 67, \bold{74}
@@ -564,7 +563,7 @@
\item {\tt resolve_tac}, \bold{17}, 131
\item {\tt restore_proof}, \bold{15}
\item {\tt result}, \bold{9}, 16, 57
- \item {\tt rev_mp} theorem, \bold{101}
+ \item {\tt rev_mp} theorem, \bold{102}
\item rewrite rules, 107--108
\subitem permutative, 117--120
\item {\tt rewrite_goals_rule}, \bold{39}
@@ -677,14 +676,14 @@
\item {\tt subgoal_tac}, \bold{20}
\item {\tt subgoals_of_brl}, \bold{24}
\item {\tt subgoals_tac}, \bold{20}
- \item {\tt subst} theorem, 99, \bold{101}
+ \item {\tt subst} theorem, 99, \bold{102}
\item substitution
\subitem rules, 99
\item {\tt subthy}, \bold{58}
\item {\tt swap} theorem, \bold{139}
\item {\tt swap_res_tac}, \bold{138}
\item {\tt swapify}, \bold{138}
- \item {\tt sym} theorem, 100, \bold{101}
+ \item {\tt sym} theorem, 100, \bold{102}
\item {\tt symmetric}, \bold{44}
\item {\tt syn_of}, \bold{72}
\item syntax
@@ -772,6 +771,7 @@
\item {\tt theory} ML type, 51
\item {\tt Theory.add_oracle}, \bold{64}
\item {\tt theory_of_thm}, \bold{41}
+ \item {\tt thin_refl} theorem, \bold{102}
\item {\tt thin_tac}, \bold{23}
\item {\tt THM} exception, 37, 38, 42, 47
\item {\tt thm} ML type, 37
@@ -827,7 +827,6 @@
\item type unknowns, \bold{63}, 70
\subitem freezing/thawing of, 46
\item type variables, \bold{63}
- \item {\tt typed_print_translation}, 95
\item types, \bold{63}
\subitem certified, \bold{63}
\subitem printing of, 4, 15, 63
--- a/doc-src/Ref/simplifier.tex Thu Feb 05 10:26:16 1998 +0100
+++ b/doc-src/Ref/simplifier.tex Thu Feb 05 10:26:59 1998 +0100
@@ -91,13 +91,13 @@
by (Asm_simp_tac 1);
\end{ttbox}
-\medskip {\tt Asm_full_simp_tac} is the most powerful of this quartet
+\medskip \texttt{Asm_full_simp_tac} is the most powerful of this quartet
of tactics but may also loop where some of the others terminate. For
example,
\begin{ttbox}
{\out 1. ALL x. f x = g (f (g x)) ==> f 0 = f 0 + 0}
\end{ttbox}
-is solved by {\tt Simp_tac}, but {\tt Asm_simp_tac} and {\tt
+is solved by \texttt{Simp_tac}, but \texttt{Asm_simp_tac} and {\tt
Asm_simp_tac} loop because the rewrite rule $f\,\Var{x} =
g\,(f\,(g\,\Var{x}))$ extracted from the assumption does not
terminate. Isabelle notices certain simple forms of nontermination,
@@ -366,10 +366,10 @@
\begin{ttdescription}
-\item[$ss$ \ttindexbold{addsimprocs} $procs$] adds simplification
+\item[$ss$ \ttindexbold{addsimprocs} $procs$] adds the simplification
procedures $procs$ to the current simpset.
-\item[$ss$ \ttindexbold{delsimprocs} $procs$] deletes simplification
+\item[$ss$ \ttindexbold{delsimprocs} $procs$] deletes the simplification
procedures $procs$ from the current simpset.
\end{ttdescription}
@@ -505,7 +505,7 @@
The solver is a pair of tactics that attempt to solve a subgoal after
simplification. Typically it just proves trivial subgoals such as
-{\tt True} and $t=t$. It could use sophisticated means such as {\tt
+\texttt{True} and $t=t$. It could use sophisticated means such as {\tt
blast_tac}, though that could make simplification expensive.
Rewriting does not instantiate unknowns. For example, rewriting
@@ -564,7 +564,7 @@
the solver. For this reason, solver tactics must be prepared to solve
goals of the form $t = \Var{x}$, usually by reflexivity. In
particular, reflexivity should be tried before any of the fancy
-tactics like {\tt blast_tac}.
+tactics like \texttt{blast_tac}.
It may even happen that due to simplification the subgoal is no longer
an equality. For example $False \bimp \Var{Q}$ could be rewritten to
@@ -846,7 +846,7 @@
{\out val prem = "f(Suc(?n)) = Suc(f(?n))}
{\out [!!n. f(Suc(n)) = Suc(f(n))]" : thm}
\end{ttbox}
-In the theorem~{\tt prem}, note that $f$ is a free variable while
+In the theorem~\texttt{prem}, note that $f$ is a free variable while
$\Var{n}$ is a schematic variable.
\begin{ttbox}
by (res_inst_tac [("n","i")] induct 1);
@@ -958,7 +958,7 @@
\item To complete your set of rewrite rules, you must add not just
associativity~(A) and commutativity~(C) but also a derived rule, {\bf
- left-commutativity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.
+ left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.
\end{itemize}
Ordered rewriting with the combination of A, C, and~LC sorts a term
lexicographically:
@@ -973,14 +973,14 @@
This example is again set in \HOL\ (see \texttt{HOL/ex/NatSum}).
Theory \thydx{Arith} contains natural numbers arithmetic. Its
associated simpset contains many arithmetic laws including
-distributivity of~$\times$ over~$+$, while {\tt add_ac} is a list
+distributivity of~$\times$ over~$+$, while \texttt{add_ac} is a list
consisting of the A, C and LC laws for~$+$ on type \texttt{nat}. Let
us prove the theorem
\[ \sum@{i=1}^n i = n\times(n+1)/2. \]
%
-A functional~{\tt sum} represents the summation operator under the
-interpretation ${\tt sum} \, f \, (n + 1) = \sum@{i=0}^n f\,i$. We
-extend {\tt Arith} as follows:
+A functional~\texttt{sum} represents the summation operator under the
+interpretation $\texttt{sum} \, f \, (n + 1) = \sum@{i=0}^n f\,i$. We
+extend \texttt{Arith} as follows:
\begin{ttbox}
NatSum = Arith +
consts sum :: [nat=>nat, nat] => nat
@@ -997,7 +997,7 @@
Delsimprocs nat_cancel;
Addsimps add_ac;
\end{ttbox}
-Our desired theorem now reads ${\tt sum} \, (\lambda i.i) \, (n+1) =
+Our desired theorem now reads $\texttt{sum} \, (\lambda i.i) \, (n+1) =
n\times(n+1)/2$. The Isabelle goal has both sides multiplied by~$2$:
\begin{ttbox}
goal NatSum.thy "2 * sum (\%i.i) (Suc n) = n * Suc n";
@@ -1032,7 +1032,7 @@
{\out 2 * sum (\%i. i) (Suc n) = n * Suc n}
{\out No subgoals!}
\end{ttbox}
-Simplification cannot prove the induction step if we omit {\tt add_ac} from
+Simplification cannot prove the induction step if we omit \texttt{add_ac} from
the simpset. Observe that like terms have not been collected:
\begin{ttbox}
{\out Level 3}
@@ -1050,7 +1050,7 @@
\subsection{Re-orienting equalities}
-Ordered rewriting with the derived rule {\tt symmetry} can reverse
+Ordered rewriting with the derived rule \texttt{symmetry} can reverse
equations:
\begin{ttbox}
val symmetry = prove_goal HOL.thy "(x=y) = (y=x)"
@@ -1058,16 +1058,16 @@
\end{ttbox}
This is frequently useful. Assumptions of the form $s=t$, where $t$ occurs
in the conclusion but not~$s$, can often be brought into the right form.
-For example, ordered rewriting with {\tt symmetry} can prove the goal
+For example, ordered rewriting with \texttt{symmetry} can prove the goal
\[ f(a)=b \conj f(a)=c \imp b=c. \]
-Here {\tt symmetry} reverses both $f(a)=b$ and $f(a)=c$
+Here \texttt{symmetry} reverses both $f(a)=b$ and $f(a)=c$
because $f(a)$ is lexicographically greater than $b$ and~$c$. These
re-oriented equations, as rewrite rules, replace $b$ and~$c$ in the
conclusion by~$f(a)$.
Another example is the goal $\neg(t=u) \imp \neg(u=t)$.
The differing orientations make this appear difficult to prove. Ordered
-rewriting with {\tt symmetry} makes the equalities agree. (Without
+rewriting with \texttt{symmetry} makes the equalities agree. (Without
knowing more about~$t$ and~$u$ we cannot say whether they both go to $t=u$
or~$u=t$.) Then the simplifier can prove the goal outright.
@@ -1126,7 +1126,8 @@
\begin{ttbox}
local
val lhss =
- [read_cterm (sign_of Prod.thy) ("f::'a*'b=>'c", TVar (("'z", 0), []))];
+ [read_cterm (sign_of Prod.thy)
+ ("f::'a*'b=>'c", TVar (("'z", 0), []))];
val rew = mk_meta_eq pair_eta_expand; \medskip
fun proc _ _ (Abs _) = Some rew
| proc _ _ _ = None;
@@ -1165,10 +1166,10 @@
use "$ISABELLE_HOME/src/Provers/splitter.ML";
\end{ttbox}
-Simplification requires reflecting various object-equalities to
-meta-level rewrite rules. This demands rules stating that equal terms
-and equivalent formulae are also equal at the meta-level. The rule
-declaration part of the file {\tt FOL/IFOL.thy} contains the two lines
+Simplification requires converting object-equalities to meta-level rewrite
+rules. This demands rules stating that equal terms and equivalent formulae
+are also equal at the meta-level. The rule declaration part of the file
+\texttt{FOL/IFOL.thy} contains the two lines
\begin{ttbox}\index{*eq_reflection theorem}\index{*iff_reflection theorem}
eq_reflection "(x=y) ==> (x==y)"
iff_reflection "(P<->Q) ==> (P==Q)"
@@ -1177,7 +1178,7 @@
particular logic. In Constructive Type Theory, equality is a ternary
relation of the form $a=b\in A$; the type~$A$ determines the meaning
of the equality essentially as a partial equivalence relation. The
-present simplifier cannot be used. Rewriting in {\tt CTT} uses
+present simplifier cannot be used. Rewriting in \texttt{CTT} uses
another simplifier, which resides in the file {\tt
Provers/typedsimp.ML} and is not documented. Even this does not
work for later variants of Constructive Type Theory that use
@@ -1198,7 +1199,7 @@
(IntPr.fast_tac 1) ]));
\end{ttbox}
The following rewrite rules about conjunction are a selection of those
-proved on {\tt FOL/simpdata.ML}. Later, these will be supplied to the
+proved on \texttt{FOL/simpdata.ML}. Later, these will be supplied to the
standard simpset.
\begin{ttbox}
val conj_simps = map int_prove_fun
@@ -1225,20 +1226,20 @@
setmksimps : simpset * (thm -> thm list) -> simpset \hfill{\bf infix 4}
\end{ttbox}
The next step is to define the function for preprocessing rewrite rules.
-This will be installed by calling {\tt setmksimps} below. Preprocessing
+This will be installed by calling \texttt{setmksimps} below. Preprocessing
occurs whenever rewrite rules are added, whether by user command or
automatically. Preprocessing involves extracting atomic rewrites at the
object-level, then reflecting them to the meta-level.
-To start, the function {\tt gen_all} strips any meta-level
+To start, the function \texttt{gen_all} strips any meta-level
quantifiers from the front of the given theorem. Usually there are none
anyway.
\begin{ttbox}
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
\end{ttbox}
-The function {\tt atomize} analyses a theorem in order to extract
+The function \texttt{atomize} analyses a theorem in order to extract
atomic rewrite rules. The head of all the patterns, matched by the
-wildcard~{\tt _}, is the coercion function {\tt Trueprop}.
+wildcard~\texttt{_}, is the coercion function \texttt{Trueprop}.
\begin{ttbox}
fun atomize th = case concl_of th of
_ $ (Const("op &",_) $ _ $ _) => atomize(th RS conjunct1) \at
@@ -1260,21 +1261,21 @@
\item Universal quantification: remove the quantifier, replacing the bound
variable by a schematic variable, and extract rewrites from the body.
-\item {\tt True} and {\tt False} contain no useful rewrites.
+\item \texttt{True} and \texttt{False} contain no useful rewrites.
\item Anything else: return the theorem in a singleton list.
\end{itemize}
The resulting theorems are not literally atomic --- they could be
disjunctive, for example --- but are broken down as much as possible. See
-the file {\tt ZF/simpdata.ML} for a sophisticated translation of
+the file \texttt{ZF/simpdata.ML} for a sophisticated translation of
set-theoretic formulae into rewrite rules.
The simplified rewrites must now be converted into meta-equalities. The
-rule {\tt eq_reflection} converts equality rewrites, while {\tt
+rule \texttt{eq_reflection} converts equality rewrites, while {\tt
iff_reflection} converts if-and-only-if rewrites. The latter possibility
can arise in two other ways: the negative theorem~$\neg P$ is converted to
-$P\equiv{\tt False}$, and any other theorem~$P$ is converted to
-$P\equiv{\tt True}$. The rules {\tt iff_reflection_F} and {\tt
+$P\equiv\texttt{False}$, and any other theorem~$P$ is converted to
+$P\equiv\texttt{True}$. The rules \texttt{iff_reflection_F} and {\tt
iff_reflection_T} accomplish this conversion.
\begin{ttbox}
val P_iff_F = int_prove_fun "~P ==> (P <-> False)";
@@ -1283,7 +1284,7 @@
val P_iff_T = int_prove_fun "P ==> (P <-> True)";
val iff_reflection_T = P_iff_T RS iff_reflection;
\end{ttbox}
-The function {\tt mk_meta_eq} converts a theorem to a meta-equality
+The function \texttt{mk_meta_eq} converts a theorem to a meta-equality
using the case analysis described above.
\begin{ttbox}
fun mk_meta_eq th = case concl_of th of
@@ -1292,13 +1293,13 @@
| _ $ (Const("Not",_)$_) => th RS iff_reflection_F
| _ => th RS iff_reflection_T;
\end{ttbox}
-The three functions {\tt gen_all}, {\tt atomize} and {\tt mk_meta_eq} will
-be composed together and supplied below to {\tt setmksimps}.
+The three functions \texttt{gen_all}, \texttt{atomize} and \texttt{mk_meta_eq} will
+be composed together and supplied below to \texttt{setmksimps}.
\subsection{Making the initial simpset}
-It is time to assemble these items. We open module {\tt Simplifier}
+It is time to assemble these items. We open module \texttt{Simplifier}
to gain direct access to its components. We define the infix operator
\ttindex{addcongs} to insert congruence rules; given a list of
theorems, it converts their conclusions into meta-equalities and
@@ -1317,16 +1318,16 @@
fun ss addsplits splits = ss addloop (split_tac splits);
\end{ttbox}
-The list {\tt IFOL_simps} contains the default rewrite rules for
-first-order logic. The first of these is the reflexive law expressed
-as the equivalence $(a=a)\bimp{\tt True}$; the rewrite rule $a=a$ is
+The list \texttt{IFOL_simps} contains the default rewrite rules for
+intuitionistic first-order logic. The first of these is the reflexive law
+expressed as the equivalence $(a=a)\bimp\texttt{True}$; the rewrite rule $a=a$ is
clearly useless.
\begin{ttbox}
val IFOL_simps =
[refl RS P_iff_T] \at conj_simps \at disj_simps \at not_simps \at
imp_simps \at iff_simps \at quant_simps;
\end{ttbox}
-The list {\tt triv_rls} contains trivial theorems for the solver. Any
+The list \texttt{triv_rls} contains trivial theorems for the solver. Any
subgoal that is simplified to one of these will be removed.
\begin{ttbox}
val notFalseI = int_prove_fun "~False";
@@ -1335,15 +1336,15 @@
%
The basic simpset for intuitionistic \FOL{} is
\ttindexbold{FOL_basic_ss}. It preprocess rewrites using {\tt
- gen_all}, {\tt atomize} and {\tt mk_meta_eq}. It solves simplified
-subgoals using {\tt triv_rls} and assumptions, and by detecting
+ gen_all}, \texttt{atomize} and \texttt{mk_meta_eq}. It solves simplified
+subgoals using \texttt{triv_rls} and assumptions, and by detecting
contradictions. It uses \ttindex{asm_simp_tac} to tackle subgoals of
conditional rewrites.
-Other simpsets built from {\tt FOL_basic_ss} will inherit these items.
+Other simpsets built from \texttt{FOL_basic_ss} will inherit these items.
In particular, \ttindexbold{IFOL_ss}, which introduces {\tt
IFOL_simps} as rewrite rules. \ttindexbold{FOL_ss} will later
-extend {\tt IFOL_ss} with classical rewrite rules such as $\neg\neg
+extend \texttt{IFOL_ss} with classical rewrite rules such as $\neg\neg
P\bimp P$.
\index{*setmksimps}\index{*setSSolver}\index{*setSolver}\index{*setsubgoaler}
\index{*addsimps}\index{*addcongs}
@@ -1355,20 +1356,22 @@
eq_assume_tac, ematch_tac [FalseE]];
val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
- addsimprocs [defALL_regroup,defEX_regroup]
+ addsimprocs [defALL_regroup, defEX_regroup]
setSSolver safe_solver
setSolver unsafe_solver
- setmksimps (map mk_meta_eq o atomize o gen_all);
+ setmksimps (map mk_meta_eq o
+ atomize o gen_all);
-val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps {\at} int_ex_simps {\at} int_all_simps)
+val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps {\at}
+ int_ex_simps {\at} int_all_simps)
addcongs [imp_cong];
\end{ttbox}
-This simpset takes {\tt imp_cong} as a congruence rule in order to use
+This simpset takes \texttt{imp_cong} as a congruence rule in order to use
contextual information to simplify the conclusions of implications:
\[ \List{\Var{P}\bimp\Var{P'};\; \Var{P'} \Imp \Var{Q}\bimp\Var{Q'}} \Imp
(\Var{P}\imp\Var{Q}) \bimp (\Var{P'}\imp\Var{Q'})
\]
-By adding the congruence rule {\tt conj_cong}, we could obtain a similar
+By adding the congruence rule \texttt{conj_cong}, we could obtain a similar
effect for conjunctions.
@@ -1376,7 +1379,7 @@
To set up case splitting, we must prove the theorem \texttt{meta_iffD}
below and pass it to \ttindexbold{mk_case_split_tac}. The tactic
-\ttindexbold{split_tac} uses {\tt mk_meta_eq}, defined above, to
+\ttindexbold{split_tac} uses \texttt{mk_meta_eq}, defined above, to
convert the splitting rules to meta-equalities.
\begin{ttbox}
val meta_iffD =
@@ -1399,7 +1402,7 @@
\langle a,b\rangle \imp \Var{P}(\Var{f}(a,b)))
\]
Case splits should be allowed only when necessary; they are expensive
-and hard to control. Here is an example of use, where {\tt expand_if}
+and hard to control. Here is an example of use, where \texttt{expand_if}
is the first rule above:
\begin{ttbox}
by (simp_tac (simpset() addloop (split_tac [expand_if])) 1);
--- a/doc-src/Ref/syntax.tex Thu Feb 05 10:26:16 1998 +0100
+++ b/doc-src/Ref/syntax.tex Thu Feb 05 10:26:59 1998 +0100
@@ -712,16 +712,13 @@
which triggers calls to it. Such names can be constants (logical or
syntactic) or type constructors.
-{\tt print_syntax} displays the sets of names associated with the
-translation functions of a theory under
-\ttindex{parse_ast_translation}, \ttindex{parse_translation},
-\ttindex{print_translation} (or \ttindex{typed_print_translation}) and
-\ttindex{print_ast_translation}. You can add new ones via the {\tt
- ML} section\index{*ML section} of a theory definition file. There
-may never be more than one function of the same kind per name. Even
-though the {\tt ML} section is the very last part of the file, newly
-installed translation functions are already effective when processing
-all of the preceding sections.
+{\tt print_syntax} displays the sets of names associated with the translation
+functions of a theory under \texttt{parse_ast_translation}, etc. You can add
+new ones via the {\tt ML} section\index{*ML section} of a theory definition
+file. There may never be more than one function of the same kind per name.
+Even though the {\tt ML} section is the very last part of the file, newly
+installed translation functions are already effective when processing all of
+the preceding sections.
The {\tt ML} section's contents are simply copied verbatim near the
beginning of the \ML\ file generated from a theory definition file.
--- a/doc-src/Ref/tactic.tex Thu Feb 05 10:26:16 1998 +0100
+++ b/doc-src/Ref/tactic.tex Thu Feb 05 10:26:59 1998 +0100
@@ -475,7 +475,7 @@
proof state are never updated (see~\S\ref{match_tac}).
\item[\ttindexbold{subgoals_of_brl}({\it flag},{\it rule})]
-returns the number of new subgoals that bi-resolution would yield for the
+returns the number of new subgoals that bi-res\-o\-lu\-tion would yield for the
pair (if applied to a suitable subgoal). This is $n$ if the flag is
{\tt false} and $n-1$ if the flag is {\tt true}, where $n$ is the number
of premises of the rule. Elim-resolution yields one fewer subgoal than
--- a/doc-src/Ref/theories.tex Thu Feb 05 10:26:16 1998 +0100
+++ b/doc-src/Ref/theories.tex Thu Feb 05 10:26:59 1998 +0100
@@ -838,7 +838,8 @@
\begin{ttbox}
invoke_oracle : theory -> xstring -> Sign.sg * object -> thm
-Theory.add_oracle : bstring * (Sign.sg * object -> term) -> theory -> theory
+Theory.add_oracle : bstring * (Sign.sg * object -> term) -> theory
+ -> theory
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{invoke_oracle} $thy$ $name$ ($sign$, $data$)]
@@ -914,8 +915,8 @@
Now in \texttt{IffOracle.ML} we first define a wrapper for invoking
the oracle:
\begin{ttbox}
-fun iff_oracle n =
- invoke_oracle IffOracle.thy "iff" (sign_of IffOracle.thy, IffOracleExn n);
+fun iff_oracle n = invoke_oracle IffOracle.thy "iff"
+ (sign_of IffOracle.thy, IffOracleExn n);
\end{ttbox}
Here are some example applications of the \texttt{iff} oracle. An
--- a/doc-src/Ref/thm.tex Thu Feb 05 10:26:16 1998 +0100
+++ b/doc-src/Ref/thm.tex Thu Feb 05 10:26:59 1998 +0100
@@ -158,7 +158,7 @@
incorrectly.
\item[\ttindexbold{read_instantiate_sg} {\it sg} {\it insts} {\it thm}]
- resembles \hbox{\tt read_instantiate {\it insts} {\it thm}}, but reads
+ is like \texttt{read_instantiate {\it insts}~{\it thm}}, but it reads
the instantiations under signature~{\it sg}. This is necessary to
instantiate a rule from a general theory, such as first-order logic,
using the notation of some specialized theory. Use the function {\tt
@@ -226,7 +226,7 @@
tpairs_of : thm -> (term*term) list
sign_of_thm : thm -> Sign.sg
theory_of_thm : thm -> theory
-dest_state : thm * int -> (term * term) list * term list * term * term
+dest_state : thm * int -> (term*term) list * term list * term * term
rep_thm : thm -> {\ttlbrace}sign_ref: Sign.sg_ref, der: deriv, maxidx: int,
shyps: sort list, hyps: term list, prop: term\ttrbrace
crep_thm : thm -> {\ttlbrace}sign_ref: Sign.sg_ref, der: deriv, maxidx: int,
@@ -778,7 +778,7 @@
\begin{ttdescription}
\item[\ttindexbold{keep_derivs} := MinDeriv $|$ ThmDeriv $|$ FullDeriv;]
-specifies one of the three options for keeping derivations. They can be
+specifies one of the options for keeping derivations. They can be
minimal (oracles only), include theorems and axioms, or be full.
\item[\ttindexbold{Deriv.size} $der$] yields the size of a derivation,