--- a/doc-src/IsarRef/generic.tex Tue Apr 04 18:08:08 2000 +0200
+++ b/doc-src/IsarRef/generic.tex Tue Apr 04 22:16:11 2000 +0200
@@ -417,8 +417,10 @@
\subsection{Declaring rules}
+\indexisarcmd{print-simpset}
\indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong}
\begin{matharray}{rcl}
+ print_simpset & : & \isarkeep{theory~|~proof} \\
simp & : & \isaratt \\
split & : & \isaratt \\
cong & : & \isaratt \\
@@ -430,6 +432,9 @@
\end{rail}
\begin{descr}
+\item [$print_simpset$] prints the collection of rules declared to the
+ Simplifier, which is also known as ``simpset'' internally
+ \cite{isabelle-ref}. This is a diagnostic command; $undo$ does not apply.
\item [$simp$] declares simplification rules.
\item [$split$] declares split rules.
\item [$cong$] declares congruence rules.
@@ -572,9 +577,11 @@
\subsection{Declaring rules}\label{sec:classical-mod}
+\indexisarcmd{print-claset}
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
\indexisaratt{iff}\indexisaratt{delrule}
\begin{matharray}{rcl}
+ print_claset & : & \isarkeep{theory~|~proof} \\
intro & : & \isaratt \\
elim & : & \isaratt \\
dest & : & \isaratt \\
@@ -589,6 +596,9 @@
\end{rail}
\begin{descr}
+\item [$print_claset$] prints the collection of rules declared to the
+ Classical Reasoner, which is also known as ``simpset'' internally
+ \cite{isabelle-ref}. This is a diagnostic command; $undo$ does not apply.
\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
destruct rules, respectively. By default, rules are considered as
\emph{safe}, while a single ``?'' classifies as \emph{unsafe}, and ``??'' as