src/Doc/Isar_Ref/Outer_Syntax.thy
changeset 63137 9553f11d67c4
parent 63120 629a4c5e953e
child 63138 70f4d67235a0
     1.1 --- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Tue May 24 15:24:32 2016 +0200
     1.2 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Tue May 24 15:53:16 2016 +0200
     1.3 @@ -222,7 +222,7 @@
     1.4    @{rail \<open>
     1.5      @{syntax_def embedded}: @{syntax cartouche} | @{syntax string} |
     1.6        @{syntax ident} | @{syntax longident} | @{syntax symident} |
     1.7 -      @{syntax nat}
     1.8 +      @{syntax var} | @{syntax typefree} | @{syntax typevar} | @{syntax nat}
     1.9    \<close>}
    1.10  \<close>
    1.11  
    1.12 @@ -278,12 +278,11 @@
    1.13    as \<^verbatim>\<open>=\<close> or \<^verbatim>\<open>+\<close>).
    1.14  
    1.15    @{rail \<open>
    1.16 -    @{syntax_def type}: @{syntax embedded} | @{syntax typefree} |
    1.17 -      @{syntax typevar}
    1.18 +    @{syntax_def type}: @{syntax embedded}
    1.19      ;
    1.20 -    @{syntax_def term}: @{syntax embedded} | @{syntax var}
    1.21 +    @{syntax_def term}: @{syntax embedded}
    1.22      ;
    1.23 -    @{syntax_def prop}: @{syntax term}
    1.24 +    @{syntax_def prop}: @{syntax embedded}
    1.25    \<close>}
    1.26  
    1.27    Positional instantiations are specified as a sequence of terms, or the