1.1 --- a/etc/isar-keywords-ZF.el	Mon Feb 03 11:07:09 2003 +0100
     1.2 +++ b/etc/isar-keywords-ZF.el	Mon Feb 03 11:08:10 2003 +0100
     1.3 @@ -103,6 +103,7 @@
     1.4      "print_context"
     1.5      "print_facts"
     1.6      "print_induct_rules"
     1.7 +    "print_intros"
     1.8      "print_locale"
     1.9      "print_locales"
    1.10      "print_methods"
    1.11 @@ -243,6 +244,7 @@
    1.12      "print_context"
    1.13      "print_facts"
    1.14      "print_induct_rules"
    1.15 +    "print_intros"
    1.16      "print_locale"
    1.17      "print_locales"
    1.18      "print_methods"

     2.1 --- a/etc/isar-keywords.el	Mon Feb 03 11:07:09 2003 +0100
     2.2 +++ b/etc/isar-keywords.el	Mon Feb 03 11:08:10 2003 +0100
     2.3 @@ -105,6 +105,7 @@
     2.4      "print_context"
     2.5      "print_facts"
     2.6      "print_induct_rules"
     2.7 +    "print_intros"
     2.8      "print_locale"
     2.9      "print_locales"
    2.10      "print_methods"
    2.11 @@ -264,6 +265,7 @@
    2.12      "print_context"
    2.13      "print_facts"
    2.14      "print_induct_rules"
    2.15 +    "print_intros"
    2.16      "print_locale"
    2.17      "print_locales"
    2.18      "print_methods"

     3.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Feb 03 11:07:09 2003 +0100
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Feb 03 11:08:10 2003 +0100
     3.3 @@ -605,6 +605,10 @@
     3.4    OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag
     3.5      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases));
     3.6  
     3.7 +val print_introsP =
     3.8 +  OuterSyntax.improper_command "print_intros" "print matching introduction rules" K.diag
     3.9 +    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_intros));
    3.10 +
    3.11  val print_thmsP =
    3.12    OuterSyntax.improper_command "thm" "print theorems" K.diag
    3.13      (opt_modes -- P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
    3.14 @@ -756,7 +760,7 @@
    3.15    print_attributesP, print_rulesP, print_induct_rulesP,
    3.16    print_trans_rulesP, print_methodsP, print_antiquotationsP,
    3.17    thms_containingP, thm_depsP, print_bindsP, print_lthmsP,
    3.18 -  print_casesP, print_thmsP, print_prfsP, print_full_prfsP,
    3.19 +  print_casesP, print_introsP, print_thmsP, print_prfsP, print_full_prfsP,
    3.20    print_propP, print_termP, print_typeP,
    3.21    (*system commands*)
    3.22    cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,