added 'print_abbrevs';
authorwenzelm
Sat Dec 09 18:05:46 2006 +0100 (2006-12-09 ago)
changeset 21726092b967da9b7
parent 21725 ec2014c93d7f
child 21727 5acd4f35d26f
added 'print_abbrevs';
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Dec 09 18:05:44 2006 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Dec 09 18:05:46 2006 +0100
     1.3 @@ -690,9 +690,13 @@
     1.4      (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory));
     1.5  
     1.6  val print_syntaxP =
     1.7 -  OuterSyntax.improper_command "print_syntax" "print inner syntax of theory (verbose!)" K.diag
     1.8 +  OuterSyntax.improper_command "print_syntax" "print inner syntax of context (verbose!)" K.diag
     1.9      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax));
    1.10  
    1.11 +val print_abbrevsP =
    1.12 +  OuterSyntax.improper_command "print_abbrevs" "print constant abbreviation of context" K.diag
    1.13 +    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_abbrevs));
    1.14 +
    1.15  val print_theoremsP =
    1.16    OuterSyntax.improper_command "print_theorems"
    1.17        "print theorems of local theory or proof context" K.diag
    1.18 @@ -938,13 +942,14 @@
    1.19    interpretationP, interpretP,
    1.20    (*diagnostic commands*)
    1.21    pretty_setmarginP, helpP, print_commandsP, print_contextP,
    1.22 -  print_theoryP, print_syntaxP, print_factsP, print_theoremsP,
    1.23 -  print_localesP, print_localeP, print_registrationsP,
    1.24 -  print_attributesP, print_simpsetP, print_rulesP,
    1.25 -  print_induct_rulesP, print_trans_rulesP, print_methodsP,
    1.26 -  print_antiquotationsP, class_depsP, thm_depsP, find_theoremsP,
    1.27 -  print_bindsP, print_casesP, print_stmtsP, print_thmsP, print_prfsP,
    1.28 -  print_full_prfsP, print_propP, print_termP, print_typeP,
    1.29 +  print_theoryP, print_syntaxP, print_abbrevsP, print_factsP,
    1.30 +  print_theoremsP, print_localesP, print_localeP,
    1.31 +  print_registrationsP, print_attributesP, print_simpsetP,
    1.32 +  print_rulesP, print_induct_rulesP, print_trans_rulesP,
    1.33 +  print_methodsP, print_antiquotationsP, class_depsP, thm_depsP,
    1.34 +  find_theoremsP, print_bindsP, print_casesP, print_stmtsP,
    1.35 +  print_thmsP, print_prfsP, print_full_prfsP, print_propP,
    1.36 +  print_termP, print_typeP,
    1.37    (*system commands*)
    1.38    cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
    1.39    touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,