added print_rules;
authorwenzelm
Wed, 05 Dec 2001 03:15:50 +0100
changeset 12382 8896d7f49422
parent 12381 5177845a34f5
child 12383 af14fd56b189
added print_rules;
src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Dec 05 03:15:32 2001 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Dec 05 03:15:50 2001 +0100
@@ -49,6 +49,7 @@
   val print_locales: Toplevel.transition -> Toplevel.transition
   val print_locale: Locale.expr -> Toplevel.transition -> Toplevel.transition
   val print_attributes: Toplevel.transition -> Toplevel.transition
+  val print_rules: Toplevel.transition -> Toplevel.transition
   val print_induct_rules: Toplevel.transition -> Toplevel.transition
   val print_trans_rules: Toplevel.transition -> Toplevel.transition
   val print_methods: Toplevel.transition -> Toplevel.transition
@@ -198,6 +199,10 @@
 val print_attributes = Toplevel.unknown_theory o
   Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
 
+val print_rules = Toplevel.unknown_context o
+  Toplevel.keep (Toplevel.node_case ContextRules.print_global_rules
+    (ContextRules.print_local_rules o Proof.context_of));
+
 val print_induct_rules = Toplevel.unknown_context o
   Toplevel.keep (Toplevel.node_case InductAttrib.print_global_rules
     (InductAttrib.print_local_rules o Proof.context_of));