# HG changeset patch
# User berghofe
# Date 1044266890 -3600
# Node ID ebed89f74e59c3540876736a26c4a4ad88dded61
# Parent  6c5c5bdfae84ead5774515a2dcb65cab1dbd13e2
Added "print_intros" command.

diff -r 6c5c5bdfae84 -r ebed89f74e59 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Mon Feb 03 11:07:09 2003 +0100
+++ b/etc/isar-keywords-ZF.el	Mon Feb 03 11:08:10 2003 +0100
@@ -103,6 +103,7 @@
     "print_context"
     "print_facts"
     "print_induct_rules"
+    "print_intros"
     "print_locale"
     "print_locales"
     "print_methods"
@@ -243,6 +244,7 @@
     "print_context"
     "print_facts"
     "print_induct_rules"
+    "print_intros"
     "print_locale"
     "print_locales"
     "print_methods"
diff -r 6c5c5bdfae84 -r ebed89f74e59 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Mon Feb 03 11:07:09 2003 +0100
+++ b/etc/isar-keywords.el	Mon Feb 03 11:08:10 2003 +0100
@@ -105,6 +105,7 @@
     "print_context"
     "print_facts"
     "print_induct_rules"
+    "print_intros"
     "print_locale"
     "print_locales"
     "print_methods"
@@ -264,6 +265,7 @@
     "print_context"
     "print_facts"
     "print_induct_rules"
+    "print_intros"
     "print_locale"
     "print_locales"
     "print_methods"
diff -r 6c5c5bdfae84 -r ebed89f74e59 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Feb 03 11:07:09 2003 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Mon Feb 03 11:08:10 2003 +0100
@@ -605,6 +605,10 @@
   OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases));
 
+val print_introsP =
+  OuterSyntax.improper_command "print_intros" "print matching introduction rules" K.diag
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_intros));
+
 val print_thmsP =
   OuterSyntax.improper_command "thm" "print theorems" K.diag
     (opt_modes -- P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
@@ -756,7 +760,7 @@
   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_casesP, print_introsP, 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,