# HG changeset patch
# User wenzelm
# Date 1007518603 -3600
# Node ID af14fd56b18940616eabc55808413b0337ddac7a
# Parent  8896d7f494225142abc9561eb405c539dbaaa327
added 'print_rules' command;

diff -r 8896d7f49422 -r af14fd56b189 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Dec 05 03:15:50 2001 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Dec 05 03:16:43 2001 +0100
@@ -565,6 +565,10 @@
   OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));
 
+val print_rulesP =
+  OuterSyntax.improper_command "print_rules" "print intro/elim rules" K.diag
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_rules));
+
 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));
@@ -750,17 +754,17 @@
   (*diagnostic commands*)
   pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
   print_syntaxP, print_theoremsP, print_localesP, print_localeP,
-  print_attributesP, 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,
+  print_attributesP, print_rulesP, 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,
   kill_thyP, prP, disable_prP, enable_prP, commitP, quitP, exitP,
   init_toplevelP, welcomeP];
 
-
 end;