1.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Oct 04 11:29:25 2001 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Oct 04 11:29:46 2001 +0200
     1.3 @@ -47,6 +47,7 @@
     1.4    val print_syntax: Toplevel.transition -> Toplevel.transition
     1.5    val print_theorems: Toplevel.transition -> Toplevel.transition
     1.6    val print_attributes: Toplevel.transition -> Toplevel.transition
     1.7 +  val print_induct_rules: Toplevel.transition -> Toplevel.transition
     1.8    val print_trans_rules: Toplevel.transition -> Toplevel.transition
     1.9    val print_methods: Toplevel.transition -> Toplevel.transition
    1.10    val print_antiquotations: Toplevel.transition -> Toplevel.transition
    1.11 @@ -188,6 +189,10 @@
    1.12  val print_attributes = Toplevel.unknown_theory o
    1.13    Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
    1.14  
    1.15 +val print_induct_rules = Toplevel.unknown_context o
    1.16 +  Toplevel.keep (Toplevel.node_case InductAttrib.print_global_rules
    1.17 +    (InductAttrib.print_local_rules o Proof.context_of));
    1.18 +
    1.19  val print_trans_rules = Toplevel.unknown_context o
    1.20    Toplevel.keep (Toplevel.node_case Calculation.print_global_rules
    1.21      (Calculation.print_local_rules o Proof.context_of));

     2.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Oct 04 11:29:25 2001 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Oct 04 11:29:46 2001 +0200
     2.3 @@ -527,8 +527,12 @@
     2.4    OuterSyntax.improper_command "print_attributes" "print attributes known in this theory" K.diag
     2.5      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));
     2.6  
     2.7 +val print_induct_rulesP =
     2.8 +  OuterSyntax.improper_command "print_induct_rules" "print induction and cases rules" K.diag
     2.9 +    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_induct_rules));
    2.10 +
    2.11  val print_trans_rulesP =
    2.12 -  OuterSyntax.improper_command "print_trans_rules" "print transitivity rules in this theory" K.diag
    2.13 +  OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" K.diag
    2.14      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules));
    2.15  
    2.16  val print_methodsP =
    2.17 @@ -704,10 +708,10 @@
    2.18    (*diagnostic commands*)
    2.19    pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
    2.20    print_syntaxP, print_theoremsP, print_attributesP,
    2.21 -  print_trans_rulesP, print_methodsP, print_antiquotationsP,
    2.22 -  thms_containingP, thm_depsP, print_bindsP, print_lthmsP,
    2.23 -  print_casesP, print_thmsP, print_prfsP, print_full_prfsP,
    2.24 -  print_propP, print_termP, print_typeP,
    2.25 +  print_induct_rulesP, print_trans_rulesP, print_methodsP,
    2.26 +  print_antiquotationsP, thms_containingP, thm_depsP, print_bindsP,
    2.27 +  print_lthmsP, print_casesP, print_thmsP, print_prfsP,
    2.28 +  print_full_prfsP, print_propP, print_termP, print_typeP,
    2.29    (*system commands*)
    2.30    cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
    2.31    touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,