# HG changeset patch
# User wenzelm
# Date 1002187786 -7200
# Node ID 60d9f1069fa9fd33e24370dd62c140dccfa707ce
# Parent  7324f018ea159079d922b2860dc34d0443d05398
added print_induct_rules;

diff -r 7324f018ea15 -r 60d9f1069fa9 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Oct 04 11:29:25 2001 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Oct 04 11:29:46 2001 +0200
@@ -47,6 +47,7 @@
   val print_syntax: Toplevel.transition -> Toplevel.transition
   val print_theorems: Toplevel.transition -> Toplevel.transition
   val print_attributes: 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
   val print_antiquotations: Toplevel.transition -> Toplevel.transition
@@ -188,6 +189,10 @@
 val print_attributes = Toplevel.unknown_theory o
   Toplevel.keep (Attrib.print_attributes o Toplevel.theory_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));
+
 val print_trans_rules = Toplevel.unknown_context o
   Toplevel.keep (Toplevel.node_case Calculation.print_global_rules
     (Calculation.print_local_rules o Proof.context_of));
diff -r 7324f018ea15 -r 60d9f1069fa9 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Oct 04 11:29:25 2001 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Oct 04 11:29:46 2001 +0200
@@ -527,8 +527,12 @@
   OuterSyntax.improper_command "print_attributes" "print attributes known in this theory" K.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));
 
+val print_induct_rulesP =
+  OuterSyntax.improper_command "print_induct_rules" "print induction and cases rules" K.diag
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_induct_rules));
+
 val print_trans_rulesP =
-  OuterSyntax.improper_command "print_trans_rules" "print transitivity rules in this theory" K.diag
+  OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" K.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules));
 
 val print_methodsP =
@@ -704,10 +708,10 @@
   (*diagnostic commands*)
   pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
   print_syntaxP, print_theoremsP, print_attributesP,
-  print_trans_rulesP, print_methodsP, print_antiquotationsP,
-  thms_containingP, thm_depsP, print_bindsP, print_lthmsP,
-  print_casesP, print_thmsP, print_prfsP, print_full_prfsP,
-  print_propP, print_termP, print_typeP,
+  print_induct_rulesP, print_trans_rulesP, print_methodsP,
+  print_antiquotationsP, thms_containingP, thm_depsP, print_bindsP,
+  print_lthmsP, print_casesP, print_thmsP, print_prfsP,
+  print_full_prfsP, print_propP, print_termP, print_typeP,
   (*system commands*)
   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
   touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,