# HG changeset patch
# User wenzelm
# Date 906729667 -7200
# Node ID 620130d6b8e6c62e8713b6c9fddf5305208881a7
# Parent  defb086883a9223965f20a384d6c1fb460249719
rearranged SIMPSET(');

diff -r defb086883a9 -r 620130d6b8e6 doc-src/Ref/ref.ind
--- a/doc-src/Ref/ref.ind	Fri Sep 25 14:54:49 1998 +0200
+++ b/doc-src/Ref/ref.ind	Fri Sep 25 15:21:07 1998 +0200
@@ -3,7 +3,7 @@
   \item {\tt !!} symbol, 70
   \item {\tt\$}, \bold{61}, 87
   \item {\tt\%} symbol, 70
-  \item * SplitterFun, 127
+  \item * SplitterFun, 128
   \item {\tt ::} symbol, 70, 71
   \item {\tt ==} symbol, 70
   \item {\tt ==>} symbol, 70
@@ -29,10 +29,10 @@
   \item {\tt addaltern}, \bold{136}
   \item {\tt addbefore}, \bold{136}
   \item {\tt Addcongs}, \bold{106}
-  \item {\tt addcongs}, \bold{110}, 126, 127
+  \item {\tt addcongs}, \bold{111}, 126, 127
   \item {\tt AddDs}, \bold{141}
   \item {\tt addDs}, \bold{134}
-  \item {\tt addeqcongs}, \bold{110}, 126
+  \item {\tt addeqcongs}, \bold{111}, 127
   \item {\tt AddEs}, \bold{141}
   \item {\tt addEs}, \bold{134}
   \item {\tt AddIs}, \bold{141}
@@ -45,14 +45,14 @@
   \item {\tt AddSEs}, \bold{141}
   \item {\tt addSEs}, \bold{134}
   \item {\tt Addsimprocs}, \bold{106}
-  \item {\tt addsimprocs}, \bold{109}
+  \item {\tt addsimprocs}, \bold{110}
   \item {\tt Addsimps}, \bold{106}
   \item {\tt addsimps}, \bold{109}, 127
   \item {\tt AddSIs}, \bold{141}
   \item {\tt addSIs}, \bold{134}
   \item {\tt addSolver}, \bold{112}
   \item {\tt Addsplits}, \bold{106}
-  \item {\tt addsplits}, \bold{113}, 114
+  \item {\tt addsplits}, 114, \bold{114}
   \item {\tt addss}, \bold{136}, 137
   \item {\tt addSSolver}, \bold{112}
   \item {\tt addSWrapper}, \bold{136}
@@ -73,11 +73,11 @@
   \item arities
     \subitem context conditions, 56
   \item {\tt Asm_full_simp_tac}, \bold{105}
-  \item {\tt asm_full_simp_tac}, 25, \bold{114}, 119
+  \item {\tt asm_full_simp_tac}, 25, \bold{115}, 119
   \item {\tt asm_full_simplify}, 115
   \item {\tt asm_rl} theorem, 24
-  \item {\tt Asm_simp_tac}, \bold{104}, 116
-  \item {\tt asm_simp_tac}, \bold{114}, 127
+  \item {\tt Asm_simp_tac}, \bold{104}, 117
+  \item {\tt asm_simp_tac}, \bold{115}, 127
   \item {\tt asm_simplify}, 115
   \item associative-commutative operators, 120
   \item {\tt assume}, \bold{46}
@@ -87,7 +87,7 @@
   \item assumptions
     \subitem contradictory, 141
     \subitem deleting, 25
-    \subitem in simplification, 104, 112
+    \subitem in simplification, 104, 113
     \subitem inserting, 22
     \subitem negated, 131
     \subitem of main goal, 8, 9, 11, 16, 17
@@ -202,14 +202,14 @@
   \item definitions, \see{rewriting, meta-level}{1}, 23, \bold{56}
     \subitem unfolding, 8, 9
   \item {\tt Delcongs}, \bold{106}
-  \item {\tt delcongs}, \bold{110}
-  \item {\tt deleqcongs}, \bold{110}
+  \item {\tt delcongs}, \bold{111}
+  \item {\tt deleqcongs}, \bold{111}
   \item {\tt delete_tmpfiles}, \bold{57}
   \item delimiters, \bold{71}, 74, 75, 77
   \item {\tt delloop}, \bold{113}
   \item {\tt delrules}, \bold{134}
   \item {\tt Delsimprocs}, \bold{106}
-  \item {\tt delsimprocs}, \bold{109}
+  \item {\tt delsimprocs}, \bold{110}
   \item {\tt Delsimps}, \bold{106}
   \item {\tt delsimps}, \bold{109}
   \item {\tt Delsplits}, \bold{106}
@@ -326,7 +326,7 @@
   \item {\tt freezeT}, \bold{48}
   \item {\tt frs}, \bold{14}
   \item {\tt Full_simp_tac}, \bold{104}
-  \item {\tt full_simp_tac}, \bold{114}
+  \item {\tt full_simp_tac}, \bold{115}
   \item {\tt full_simplify}, 115
   \item {\textit {fun}} type, 64
   \item function applications, \bold{61}
@@ -476,7 +476,7 @@
   \item {\tt pr}, \bold{12}
   \item {\tt premises}, \bold{8}, 16
   \item {\tt prems_of}, \bold{43}
-  \item {\tt prems_of_ss}, \bold{111}
+  \item {\tt prems_of_ss}, \bold{112}
   \item pretty printing, 75, 77--78, 94
   \item {\tt Pretty.setdepth}, \bold{4}
   \item {\tt Pretty.setmargin}, \bold{4}
@@ -579,7 +579,7 @@
   \item {\tt restore_proof}, \bold{17}
   \item {\tt result}, \bold{9}, 11, 17
   \item {\tt rev_mp} theorem, \bold{103}
-  \item rewrite rules, 108--109
+  \item rewrite rules, 109
     \subitem permutative, 119--122
   \item {\tt rewrite_goals_rule}, \bold{41}
   \item {\tt rewrite_goals_tac}, \bold{23}, 41
@@ -587,7 +587,7 @@
   \item {\tt rewrite_tac}, 9, \bold{23}
   \item rewriting
     \subitem object-level, \see{simplification}{1}
-    \subitem ordered, 119
+    \subitem ordered, 120
     \subitem syntactic, 89--95
   \item {\tt rewtac}, \bold{22}
   \item {\tt RL}, \bold{40}
@@ -604,7 +604,7 @@
 
   \indexspace
 
-  \item {\tt safe_asm_full_simp_tac}, \bold{114}
+  \item {\tt safe_asm_full_simp_tac}, \bold{115}
   \item {\tt Safe_step_tac}, \bold{141}
   \item {\tt safe_step_tac}, 135, \bold{140}
   \item {\tt Safe_tac}, \bold{141}
@@ -624,7 +624,7 @@
   \item {\tt setSolver}, \bold{112}, 127
   \item {\tt setSSolver}, \bold{112}, 127
   \item {\tt setsubgoaler}, \bold{111}, 127
-  \item {\tt settermless}, \bold{119}
+  \item {\tt settermless}, \bold{120}
   \item {\tt setup}
     \subitem simplifier, 128
     \subitem theory, 55
@@ -646,13 +646,13 @@
   \item {\tt sign_of_thm}, \bold{43}
   \item signatures, \bold{53}, 61, 63, 65
   \item {\tt Simp_tac}, \bold{104}
-  \item {\tt simp_tac}, \bold{114}
+  \item {\tt simp_tac}, \bold{115}
   \item simplification, 104--128
     \subitem conversions, 115
     \subitem forward rules, 115
     \subitem from classical reasoner, 136
-    \subitem setting up, 123
-    \subitem setting up the splitter, 127
+    \subitem setting up, 124
+    \subitem setting up the splitter, 128
     \subitem setting up the theory, 128
     \subitem tactics, 114
   \item simplification sets, 107
@@ -662,11 +662,11 @@
   \item {\tt Simplifier.rewrite}, 115
   \item {\tt Simplifier.setup}, \bold{128}
   \item {\tt simplify}, 115
-  \item {\tt SIMPSET}, \bold{114}
+  \item {\tt SIMPSET}, \bold{108}
   \item simpset
     \subitem current, 104, 108
   \item {\tt simpset}, \bold{108}
-  \item {\tt SIMPSET'}, \bold{114}
+  \item {\tt SIMPSET'}, \bold{108}
   \item {\tt simpset_of}, \bold{108}
   \item {\tt simpset_ref}, \bold{108}
   \item {\tt simpset_ref_of}, \bold{108}
diff -r defb086883a9 -r 620130d6b8e6 doc-src/Ref/simplifier.tex
--- a/doc-src/Ref/simplifier.tex	Fri Sep 25 14:54:49 1998 +0200
+++ b/doc-src/Ref/simplifier.tex	Fri Sep 25 15:21:07 1998 +0200
@@ -273,6 +273,8 @@
 simpset_ref    : unit -> simpset ref
 simpset_of     : theory -> simpset
 simpset_ref_of : theory -> simpset ref
+SIMPSET        : (simpset -> tactic) -> tactic
+SIMPSET'       : (simpset -> 'a -> tactic) -> 'a -> tactic
 print_simpset  : theory -> unit
 \end{ttbox}
 
@@ -295,11 +297,26 @@
 \item[\ttindexbold{simpset_ref_of} $thy$;] retrieves the simpset
   reference variable from theory $thy$.
 
+\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.
+
 \item[\ttindexbold{print_simpset} $thy$;] prints the current simpset
   of theory $thy$ in the same way as \texttt{print_ss}.
 
 \end{ttdescription}
 
+\begin{warn}
+  There is a subtle 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}
@@ -687,8 +704,6 @@
 full_simp_tac          : simpset -> int -> tactic
 asm_full_simp_tac      : simpset -> int -> tactic
 safe_asm_full_simp_tac : simpset -> int -> tactic
-SIMPSET                : (simpset -> tactic) -> tactic
-SIMPSET'               : (simpset -> 'a -> tactic) -> 'a -> tactic
 \end{ttbox}
 
 These are the basic tactics that are underlying any actual
@@ -711,11 +726,6 @@
   building special tools, e.g.\ for combining the simplifier with the
   classical reasoner.  It is rarely used directly.
   
-\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}
 
 \medskip
@@ -743,16 +753,6 @@
 explicitly, via the above tactics used in conjunction with
 \texttt{simpset_of} or the \texttt{SIMPSET} tacticals.
 
-\begin{warn}
-  There is a subtle 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}
-
 
 \section{Forward rules and conversions}
 \index{simplification!forward rules}\index{simplification!conversions}