# HG changeset patch # User wenzelm # Date 911383184 -3600 # Node ID b9d5f5901b59c748c9eb4f1524f385765e5732d0 # Parent 5a8c731b15328b90619bbcc9619f2d7312120d8c 'prop', 'term', 'typ'; diff -r 5a8c731b1532 -r b9d5f5901b59 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Wed Nov 18 10:59:20 1998 +0100 +++ b/src/Pure/Isar/isar_syn.ML Wed Nov 18 10:59:44 1998 +0100 @@ -419,15 +419,15 @@ OuterSyntax.parser true "thm" "print theorems" (xthm >> IsarCmd.print_thms); val print_propP = - OuterSyntax.parser true "print_prop" "read and print proposition" + OuterSyntax.parser true "prop" "read and print proposition" (term >> IsarCmd.print_prop); val print_termP = - OuterSyntax.parser true "print_term" "read and print term" + OuterSyntax.parser true "term" "read and print term" (term >> IsarCmd.print_term); val print_typeP = - OuterSyntax.parser true "print_type" "read and print type" + OuterSyntax.parser true "typ" "read and print type" (typ >> IsarCmd.print_type);