print_simpset / print_claset command;

--- 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;