--- a/doc-src/Ref/simplifier.tex Tue Feb 20 13:23:58 2001 +0100
+++ b/doc-src/Ref/simplifier.tex Tue Feb 20 18:47:06 2001 +0100
@@ -1335,12 +1335,9 @@
automatically. Preprocessing involves extracting atomic rewrites at the
object-level, then reflecting them to the 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
+To start, the function \texttt{forall_elim_vars_safe} 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 \texttt{atomize} analyses a theorem in order to extract
atomic rewrite rules. The head of all the patterns, matched by the
@@ -1401,7 +1398,8 @@
| _ $ (Const("Not",_)$_) => th RS iff_reflection_F
| _ => th RS iff_reflection_T;
\end{ttbox}
-The three functions \texttt{gen_all}, \texttt{atomize} and \texttt{mk_eq}
+The
+three functions \texttt{forall_elim_vars_safe}, \texttt{atomize} and \texttt{mk_eq}
will be composed together and supplied below to \texttt{setmksimps}.
@@ -1429,7 +1427,8 @@
\end{ttbox}
%
The basic simpset for intuitionistic FOL is \ttindexbold{FOL_basic_ss}. It
-preprocess rewrites using {\tt gen_all}, \texttt{atomize} and \texttt{mk_eq}.
+preprocess rewrites using
+{\tt forall_elim_vars_safe}, \texttt{atomize} and \texttt{mk_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.
@@ -1453,7 +1452,7 @@
addsimprocs [defALL_regroup, defEX_regroup]
setSSolver safe_solver
setSolver unsafe_solver
- setmksimps (map mk_eq o atomize o gen_all)
+ setmksimps (map mk_eq o atomize o forall_elim_vars_safe)
setmkcong mk_meta_cong;
val IFOL_ss =