# HG changeset patch
# User wenzelm
# Date 911212422 -3600
# Node ID 4a75d89e281811ecbdd7b4d64ab2e305a5f69833
# Parent  457b42674b578a6042bc3d394df0af337e2fff21
thm, thms;

diff -r 457b42674b57 -r 4a75d89e2818 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Nov 16 11:33:14 1998 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Mon Nov 16 11:33:42 1998 +0100
@@ -8,7 +8,7 @@
   - constdefs;
   - axclass axioms: attribs;
   - instance: theory_to_proof (with special attribute to add result arity);
-  - witness: eliminate (!?);
+  - witness: eliminate (!);
   - result (interactive): print current result (?);
   - check evaluation of transformers (exns!);
   - 'result' command;
@@ -397,9 +397,13 @@
   OuterSyntax.parser true "print_facts" "print local theorems of proof context"
     (Scan.succeed IsarCmd.print_lthms);
 
+val print_thmsP =
+  OuterSyntax.parser true "thms" "print theorems"
+    (xname -- opt_attribs >> IsarCmd.print_thms);
+
 val print_thmP =
-  OuterSyntax.parser true "print_thm" "print stored theorem(s)"
-    (xname -- opt_attribs >> IsarCmd.print_thms);
+  OuterSyntax.parser true "thm" "print theorem"
+    (xname -- opt_attribs >> IsarCmd.print_thm);
 
 val print_propP =
   OuterSyntax.parser true "print_prop" "read and print proposition"
@@ -486,7 +490,7 @@
   (*diagnostic commands*)
   print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
   print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
-  print_thmP, print_propP, print_termP, print_typeP,
+  print_thmP, print_thmsP, print_propP, print_termP, print_typeP,
   (*system commands*)
   cdP, pwdP, use_thyP, loadP, prP, commitP, quitP, exitP, breakP];