# HG changeset patch
# User wenzelm
# Date 893949385 -7200
# Node ID 7a046198610e5a0ba45ec368dae29cc65e4f1da3
# Parent  1c502a82bcde4bdc9d4bdbc051f5d122d0175f47
fixed simpset(), claset();

diff -r 1c502a82bcde -r 7a046198610e doc-src/Logics/FOL.tex
--- a/doc-src/Logics/FOL.tex	Wed Apr 29 11:46:42 1998 +0200
+++ b/doc-src/Logics/FOL.tex	Thu Apr 30 17:16:25 1998 +0200
@@ -198,7 +198,7 @@
 \item 
 It instantiates the simplifier.  Both equality ($=$) and the biconditional
 ($\bimp$) may be used for rewriting.  Tactics such as {\tt Asm_simp_tac} and
-{\tt Full_simp_tac} use the default simpset ({\tt!simpset}), which works for
+{\tt Full_simp_tac} refer to the default simpset ({\tt simpset()}), which works for
 most purposes.  Named simplification sets include \ttindexbold{IFOL_ss},
 for intuitionistic first-order logic, and \ttindexbold{FOL_ss},
 for classical logic.  See the file
@@ -338,7 +338,7 @@
 rule (see Fig.\ts\ref{fol-cla-derived}).
 
 The classical reasoner is installed.  Tactics such as {\tt 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{FOL_cs}, which also includes quantifier
 rules.  See the file {\tt FOL/cladata.ML} for lists of the
@@ -671,10 +671,10 @@
 {\out  1. P & Q | ~ P & R}
 \end{ttbox}
 The premises (bound to the {\ML} variable {\tt prems}) are passed as
-introduction rules to \ttindex{blast_tac}.  Remember that {\tt!claset} refers
+introduction rules to \ttindex{blast_tac}.  Remember that {\tt claset()} refers
 to the default classical set.
 \begin{ttbox}
-by (blast_tac (!claset addIs prems) 1);
+by (blast_tac (claset() addIs prems) 1);
 {\out Level 1}
 {\out if(P,Q,R)}
 {\out No subgoals!}
@@ -702,7 +702,7 @@
 {\out S}
 {\out  1. P & Q | ~ P & R ==> S}
 \ttbreak
-by (blast_tac (!claset addIs prems) 1);
+by (blast_tac (claset() addIs prems) 1);
 {\out Level 2}
 {\out S}
 {\out No subgoals!}
diff -r 1c502a82bcde -r 7a046198610e doc-src/Logics/HOL.tex
--- 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!}
diff -r 1c502a82bcde -r 7a046198610e doc-src/Logics/ZF.tex
--- a/doc-src/Logics/ZF.tex	Wed Apr 29 11:46:42 1998 +0200
+++ b/doc-src/Logics/ZF.tex	Thu Apr 30 17:16:25 1998 +0200
@@ -1779,7 +1779,7 @@
 step, provided we somehow supply it with~\texttt{prem}.  We can add
 \hbox{\tt prem RS subsetD} to the claset as an introduction rule:
 \begin{ttbox}
-by (blast_tac (!claset addIs [prem RS subsetD]) 1);
+by (blast_tac (claset() addIs [prem RS subsetD]) 1);
 {\out Depth = 0}
 {\out Depth = 1}
 {\out Depth = 2}
diff -r 1c502a82bcde -r 7a046198610e doc-src/Logics/logics.ind
--- 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