--- a/src/Pure/Isar/isar_syn.ML Sat Dec 09 18:05:44 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sat Dec 09 18:05:46 2006 +0100
@@ -690,9 +690,13 @@
(opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory));
val print_syntaxP =
- OuterSyntax.improper_command "print_syntax" "print inner syntax of theory (verbose!)" K.diag
+ OuterSyntax.improper_command "print_syntax" "print inner syntax of context (verbose!)" K.diag
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax));
+val print_abbrevsP =
+ OuterSyntax.improper_command "print_abbrevs" "print constant abbreviation of context" K.diag
+ (Scan.succeed (Toplevel.no_timing o IsarCmd.print_abbrevs));
+
val print_theoremsP =
OuterSyntax.improper_command "print_theorems"
"print theorems of local theory or proof context" K.diag
@@ -938,13 +942,14 @@
interpretationP, interpretP,
(*diagnostic commands*)
pretty_setmarginP, helpP, print_commandsP, print_contextP,
- print_theoryP, print_syntaxP, print_factsP, print_theoremsP,
- print_localesP, print_localeP, print_registrationsP,
- print_attributesP, print_simpsetP, print_rulesP,
- print_induct_rulesP, print_trans_rulesP, print_methodsP,
- print_antiquotationsP, class_depsP, thm_depsP, find_theoremsP,
- print_bindsP, print_casesP, print_stmtsP, print_thmsP, print_prfsP,
- print_full_prfsP, print_propP, print_termP, print_typeP,
+ print_theoryP, print_syntaxP, print_abbrevsP, print_factsP,
+ print_theoremsP, print_localesP, print_localeP,
+ print_registrationsP, print_attributesP, print_simpsetP,
+ print_rulesP, print_induct_rulesP, print_trans_rulesP,
+ print_methodsP, print_antiquotationsP, class_depsP, thm_depsP,
+ find_theoremsP, print_bindsP, print_casesP, print_stmtsP,
+ 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,