added ML_type, ML_struct;
authorwenzelm
Sat Oct 15 00:09:07 2005 +0200 (2005-10-15)
changeset 178673368e5c72904
parent 17866 511c906c66a3
child 17868 5a12b1b5990f
added ML_type, ML_struct;
doc-src/IsarRef/syntax.tex
     1.1 --- a/doc-src/IsarRef/syntax.tex	Sat Oct 15 00:08:15 2005 +0200
     1.2 +++ b/doc-src/IsarRef/syntax.tex	Sat Oct 15 00:09:07 2005 +0200
     1.3 @@ -425,6 +425,8 @@
     1.4    prf & : & \isarantiq \\
     1.5    full_prf & : & \isarantiq \\
     1.6    ML & : & \isarantiq \\
     1.7 +  ML_type & : & \isarantiq \\
     1.8 +  ML_struct & : & \isarantiq \\
     1.9  \end{matharray}
    1.10  
    1.11  The text body of formal comments (see also \S\ref{sec:comments}) may contain
    1.12 @@ -446,6 +448,7 @@
    1.13  \indexisarant{typeof}\indexisarant{typ}\indexisarant{thm-style}
    1.14  \indexisarant{term-style}\indexisarant{text}\indexisarant{goals}
    1.15  \indexisarant{subgoals}\indexisarant{prf}\indexisarant{full-prf}\indexisarant{ML}
    1.16 +\indexisarant{ML-type}\indexisarant{ML-struct}
    1.17  
    1.18  \begin{rail}
    1.19    atsign lbrace antiquotation rbrace
    1.20 @@ -465,7 +468,9 @@
    1.21      'subgoals' options |
    1.22      'prf' options thmrefs |
    1.23      'full\_prf' options thmrefs |
    1.24 -    'ML' options name
    1.25 +    'ML' options name |
    1.26 +    'ML\_type' options name |
    1.27 +    'ML\_struct' options name
    1.28    ;
    1.29    options: '[' (option * ',') ']'
    1.30    ;
    1.31 @@ -522,8 +527,9 @@
    1.32    full proof terms, i.e.\ also displays information omitted in the compact
    1.33    proof term, which is denoted by ``$_$'' placeholders there.
    1.34    
    1.35 -\item [$\at\{ML~s\}$] checks text $s$ as an ML expression in the current
    1.36 -  runtime environment, and displays the source verbatim.
    1.37 +\item [$\at\{ML~s\}$, $\at\{ML_type~s\}$, and $\at\{ML_struct~s\}$] check text
    1.38 +  $s$ as ML value, type, and structure, respectively.  If successful, the
    1.39 +  source is displayed verbatim.
    1.40  
    1.41  \end{descr}
    1.42