--- a/doc-src/Logics/HOL.tex Wed Apr 29 11:46:42 1998 +0200
+++ b/doc-src/Logics/HOL.tex Thu Apr 30 17:16:25 1998 +0200
@@ -907,7 +907,7 @@
The simplifier is available in \HOL. Tactics such as {\tt
Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset
-({\tt!simpset}), which works for most purposes. A quite minimal
+({\tt 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
also expresses logical equivalence, may be used for rewriting. See
@@ -967,7 +967,7 @@
(analogous to \texttt{addsimps}) that adds rules such as $(*)$ to a
simpset, as in
\begin{ttbox}
-by(simp_tac (!simpset addsplits [split_if]) 1);
+by(simp_tac (simpset() addsplits [split_if]) 1);
\end{ttbox}
The effect is that after each round of simplification, one occurrence of
\texttt{if} is split acording to \texttt{split_if}, until all occurences of
@@ -978,7 +978,7 @@
you want to delete it from a simpset, use \ttindexbold{delsplits}, which is
the inverse of \texttt{addsplits}:
\begin{ttbox}
-by(simp_tac (!simpset delsplits [split_if]) 1);
+by(simp_tac (simpset() delsplits [split_if]) 1);
\end{ttbox}
In general, \texttt{addsplits} accepts rules of the form
@@ -1006,7 +1006,7 @@
rule; recall Fig.\ts\ref{hol-lemmas2} above.
The classical reasoner is installed. Tactics such as \texttt{Blast_tac} and {\tt
-Best_tac} use the default claset ({\tt!claset}), which works for most
+Best_tac} refer to the default claset ({\tt 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,
@@ -2079,7 +2079,7 @@
\item the \textit{simplification set} is used to prove that the supplied
relation is well-founded. It is also used to prove the \textbf{termination
conditions}: assertions that arguments of recursive calls decrease under
- \textit{rel}. By default, simplification uses \texttt{!simpset}, which
+ \textit{rel}. By default, simplification uses \texttt{simpset()}, which
is sufficient to prove well-foundedness for the built-in relations listed
above.
@@ -2127,7 +2127,7 @@
automatically if supplied with the right simpset.
\begin{ttbox}
recdef gcd "measure ((\%(m,n).n) ::nat*nat=>nat)"
- simpset "!simpset addsimps [mod_less_divisor, zero_less_eq]"
+ simpset "simpset() addsimps [mod_less_divisor, zero_less_eq]"
"gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
\end{ttbox}
@@ -2512,7 +2512,7 @@
{\out No subgoals!}
\end{ttbox}
How much creativity is required? As it happens, Isabelle can prove this
-theorem automatically. The default classical set {\tt!claset} contains rules
+theorem automatically. The default classical set {\tt claset()} contains rules
for most of the constructs of \HOL's set theory. We must augment it with
\tdx{equalityCE} to break up set equalities, and then apply best-first
search. Depth-first search would diverge, but best-first search
@@ -2524,7 +2524,7 @@
{\out ?S ~: range f}
{\out 1. ?S ~: range f}
\ttbreak
-by (best_tac (!claset addSEs [equalityCE]) 1);
+by (best_tac (claset() addSEs [equalityCE]) 1);
{\out Level 1}
{\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
{\out No subgoals!}
--- a/doc-src/Logics/logics.ind Wed Apr 29 11:46:42 1998 +0200
+++ b/doc-src/Logics/logics.ind Thu Apr 30 17:16:25 1998 +0200
@@ -8,9 +8,9 @@
\item {\tt\#-} symbol, 47
\item {\tt\&} symbol, 7, 60, 105
\item {\tt *} symbol, 26, 61, 79, 119
- \item {\tt *} type, 76
+ \item {\tt *} type, 77
\item {\tt +} symbol, 43, 61, 79, 119
- \item {\tt +} type, 76
+ \item {\tt +} type, 77
\item {\tt -} symbol, 25, 61, 79, 128
\item {\tt -->} symbol, 7, 60, 105, 119
\item {\tt ->} symbol, 26
@@ -49,6 +49,7 @@
\item {\tt add_unsafes}, \bold{111}
\item {\tt addC0} theorem, 128
\item {\tt addC_succ} theorem, 128
+ \item {\tt Addsplits}, \bold{76}
\item {\tt addsplits}, \bold{76}, 81, 87
\item {\tt ALL} symbol, 7, 26, 60, 62, 69, 70, 105
\item {\tt All} constant, 7, 60, 105
@@ -188,6 +189,8 @@
\item {\tt datatype}, 86--91
\item {\tt deepen_tac}, 16
+ \item {\tt Delsplits}, \bold{76}
+ \item {\tt delsplits}, \bold{76}
\item {\tt diff_0_eq_0} theorem, 128
\item {\tt Diff_cancel} theorem, 41
\item {\tt Diff_contains} theorem, 36
@@ -279,9 +282,6 @@
\item {\tt exI} theorem, 8, 66
\item {\tt exL} theorem, 107
\item {\tt Exp} theory, 100
- \item {\tt expand_if} theorem, 66, 76
- \item {\tt expand_split} theorem, 77
- \item {\tt expand_sum_case} theorem, 79
\item {\tt exR} theorem, 107, 110, 112
\item {\tt exR_thin} theorem, 108, 112, 113
\item {\tt ext} theorem, 63, 64
@@ -403,9 +403,9 @@
\item {\tt impL} theorem, 107
\item {\tt impR} theorem, 107
\item {\tt in} symbol, 27, 61
- \item {\textit {ind}} type, 80
+ \item {\textit {ind}} type, 78
\item {\tt induct} theorem, 44
- \item {\tt induct_tac}, 81, \bold{89}
+ \item {\tt induct_tac}, 80, \bold{89}
\item {\tt inductive}, 96--99
\item {\tt Inf} constant, 25, 29
\item {\tt infinity} theorem, 31
@@ -414,8 +414,8 @@
\item {\tt inj_def} theorem, 45, 75
\item {\tt inj_Inl} theorem, 79
\item {\tt inj_Inr} theorem, 79
- \item {\tt inj_onto} constant, 75
- \item {\tt inj_onto_def} theorem, 75
+ \item {\tt inj_on} constant, 75
+ \item {\tt inj_on_def} theorem, 75
\item {\tt inj_Suc} theorem, 79
\item {\tt Inl} constant, 43, 79
\item {\tt inl} constant, 117, 122, 132
@@ -568,7 +568,7 @@
\item {\tt n_not_Suc_n} theorem, 79
\item {\tt Nat} theory, 46, 80
\item {\textit {nat}} type, 79, 80, 89
- \item {\textit{nat}} type, 80--81
+ \item {\textit{nat}} type, 78--81
\item {\tt nat} constant, 47
\item {\tt nat_0I} theorem, 47
\item {\tt nat_case} constant, 47
@@ -577,9 +577,9 @@
\item {\tt nat_case_succ} theorem, 47
\item {\tt nat_def} theorem, 47
\item {\tt nat_induct} theorem, 47, 79
- \item {\tt nat_rec} constant, 81
+ \item {\tt nat_rec} constant, 80
\item {\tt nat_succI} theorem, 47
- \item {\tt NatDef} theory, 80
+ \item {\tt NatDef} theory, 78
\item {\tt NC0} theorem, 121
\item {\tt NC_succ} theorem, 121
\item {\tt NE} theorem, 120, 121, 129
@@ -655,7 +655,7 @@
\item priorities, 2
\item {\tt PROD} symbol, 26, 28, 118, 119
\item {\tt Prod} constant, 117
- \item {\tt Prod} theory, 76
+ \item {\tt Prod} theory, 77
\item {\tt ProdC} theorem, 121, 137
\item {\tt ProdC2} theorem, 121
\item {\tt ProdE} theorem, 121, 134, 136, 138
@@ -780,7 +780,10 @@
\item {\tt split_$t$_case} theorem, 87
\item {\tt split_all_tac}, \bold{78}
\item {\tt split_def} theorem, 31
+ \item {\tt split_if} theorem, 66, 76
\item {\tt split_list_case} theorem, 81
+ \item {\tt split_split} theorem, 77
+ \item {\tt split_sum_case} theorem, 79
\item {\tt ssubst} theorem, 9, 65, 67
\item {\tt stac}, \bold{75}
\item {\tt Step_tac}, 22