--- 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
--- a/src/Provers/classical.ML Tue Apr 04 18:08:08 2000 +0200
+++ b/src/Provers/classical.ML Tue Apr 04 22:16:11 2000 +0200
@@ -1181,4 +1181,16 @@
val setup = [GlobalClaset.init, LocalClaset.init, setup_attrs, setup_methods];
+
+(** outer syntax **)
+
+val print_clasetP =
+ OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
+ OuterSyntax.Keyword.diag
+ (Scan.succeed (Toplevel.keep
+ (Toplevel.node_case print_claset (print_local_claset o Proof.context_of))));
+
+val _ = OuterSyntax.add_parsers [print_clasetP];
+
+
end;
--- a/src/Provers/simplifier.ML Tue Apr 04 18:08:08 2000 +0200
+++ b/src/Provers/simplifier.ML Tue Apr 04 22:16:11 2000 +0200
@@ -550,6 +550,17 @@
in setup @ method_setup [] @ [init_ss] end;
+
+(** outer syntax **)
+
+val print_simpsetP =
+ OuterSyntax.improper_command "print_simpset" "print context of Simplifier"
+ OuterSyntax.Keyword.diag
+ (Scan.succeed (Toplevel.keep
+ (Toplevel.node_case print_simpset (print_local_simpset o Proof.context_of))));
+
+val _ = OuterSyntax.add_parsers [print_simpsetP];
+
end;