src/Pure/Isar/isar_syn.ML
changeset 11666 60d9f1069fa9
parent 11651 201b3f76c7b7
child 11742 44034a6474e5
--- 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,