'prop', 'term', 'typ';
authorwenzelm
Wed Nov 18 10:59:44 1998 +0100 (1998-11-18 ago)
changeset 5924b9d5f5901b59
parent 5923 5a8c731b1532
child 5925 669d0bc621e1
'prop', 'term', 'typ';
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Nov 18 10:59:20 1998 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Nov 18 10:59:44 1998 +0100
     1.3 @@ -419,15 +419,15 @@
     1.4    OuterSyntax.parser true "thm" "print theorems" (xthm >> IsarCmd.print_thms);
     1.5  
     1.6  val print_propP =
     1.7 -  OuterSyntax.parser true "print_prop" "read and print proposition"
     1.8 +  OuterSyntax.parser true "prop" "read and print proposition"
     1.9      (term >> IsarCmd.print_prop);
    1.10  
    1.11  val print_termP =
    1.12 -  OuterSyntax.parser true "print_term" "read and print term"
    1.13 +  OuterSyntax.parser true "term" "read and print term"
    1.14      (term >> IsarCmd.print_term);
    1.15  
    1.16  val print_typeP =
    1.17 -  OuterSyntax.parser true "print_type" "read and print type"
    1.18 +  OuterSyntax.parser true "typ" "read and print type"
    1.19      (typ >> IsarCmd.print_type);
    1.20  
    1.21