thm, thms;
authorwenzelm
Mon Nov 16 11:33:42 1998 +0100 (1998-11-16 ago)
changeset 58964a75d89e2818
parent 5895 457b42674b57
child 5897 b3548f939dd2
thm, thms;
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Nov 16 11:33:14 1998 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Nov 16 11:33:42 1998 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4    - constdefs;
     1.5    - axclass axioms: attribs;
     1.6    - instance: theory_to_proof (with special attribute to add result arity);
     1.7 -  - witness: eliminate (!?);
     1.8 +  - witness: eliminate (!);
     1.9    - result (interactive): print current result (?);
    1.10    - check evaluation of transformers (exns!);
    1.11    - 'result' command;
    1.12 @@ -397,9 +397,13 @@
    1.13    OuterSyntax.parser true "print_facts" "print local theorems of proof context"
    1.14      (Scan.succeed IsarCmd.print_lthms);
    1.15  
    1.16 +val print_thmsP =
    1.17 +  OuterSyntax.parser true "thms" "print theorems"
    1.18 +    (xname -- opt_attribs >> IsarCmd.print_thms);
    1.19 +
    1.20  val print_thmP =
    1.21 -  OuterSyntax.parser true "print_thm" "print stored theorem(s)"
    1.22 -    (xname -- opt_attribs >> IsarCmd.print_thms);
    1.23 +  OuterSyntax.parser true "thm" "print theorem"
    1.24 +    (xname -- opt_attribs >> IsarCmd.print_thm);
    1.25  
    1.26  val print_propP =
    1.27    OuterSyntax.parser true "print_prop" "read and print proposition"
    1.28 @@ -486,7 +490,7 @@
    1.29    (*diagnostic commands*)
    1.30    print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
    1.31    print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
    1.32 -  print_thmP, print_propP, print_termP, print_typeP,
    1.33 +  print_thmP, print_thmsP, print_propP, print_termP, print_typeP,
    1.34    (*system commands*)
    1.35    cdP, pwdP, use_thyP, loadP, prP, commitP, quitP, exitP, breakP];
    1.36