Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
doc-src/IsarRef/Thy/document/Inner_Syntax.tex
changeset 30240 5b25fee0362c
parent 29158 f9b3e508c27f
child 30242 aea5d7fa7ef5
equal deleted inserted replaced
30239:179ff9cb160b 30240:5b25fee0362c 
     1 %
 
     1 %
 
     2 \begin{isabellebody}%
 
     2 \begin{isabellebody}%
 
     3 \def\isabellecontext{Inner{\isacharunderscore}Syntax}%
 
     3 \def\isabellecontext{Inner{\isacharunderscore}Syntax}%
 
     4 %
 
     4 %
 
     5 \isadelimtheory
 
     5 \isadelimtheory
 
     6 \isanewline
 
       
     7 \isanewline
 
       
     8 %
 
     6 %
 
     9 \endisadelimtheory
 
     7 \endisadelimtheory
 
    10 %
 
     8 %
 
    11 \isatagtheory
 
     9 \isatagtheory
 
    12 \isacommand{theory}\isamarkupfalse%
 
    10 \isacommand{theory}\isamarkupfalse%
 
   118 }
 
   116 }
 
   119 \isamarkuptrue%
 
   117 \isamarkuptrue%
 
   120 %
 
   118 %
 
   121 \begin{isamarkuptext}%
 
   119 \begin{isamarkuptext}%
 
   122 \begin{mldecls} 
   120 \begin{mldecls} 
   123     \indexml{show\_types}\verb|show_types: bool ref| & default \verb|false| \\
 
   121     \indexdef{}{ML}{show\_types}\verb|show_types: bool ref| & default \verb|false| \\
 
   124     \indexml{show\_sorts}\verb|show_sorts: bool ref| & default \verb|false| \\
 
   122     \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool ref| & default \verb|false| \\
 
   125     \indexml{show\_consts}\verb|show_consts: bool ref| & default \verb|false| \\
 
   123     \indexdef{}{ML}{show\_consts}\verb|show_consts: bool ref| & default \verb|false| \\
 
   126     \indexml{long\_names}\verb|long_names: bool ref| & default \verb|false| \\
 
   124     \indexdef{}{ML}{long\_names}\verb|long_names: bool ref| & default \verb|false| \\
 
   127     \indexml{short\_names}\verb|short_names: bool ref| & default \verb|false| \\
 
   125     \indexdef{}{ML}{short\_names}\verb|short_names: bool ref| & default \verb|false| \\
 
   128     \indexml{unique\_names}\verb|unique_names: bool ref| & default \verb|true| \\
 
   126     \indexdef{}{ML}{unique\_names}\verb|unique_names: bool ref| & default \verb|true| \\
 
   129     \indexml{show\_brackets}\verb|show_brackets: bool ref| & default \verb|false| \\
 
   127     \indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool ref| & default \verb|false| \\
 
   130     \indexml{eta\_contract}\verb|eta_contract: bool ref| & default \verb|true| \\
 
   128     \indexdef{}{ML}{eta\_contract}\verb|eta_contract: bool ref| & default \verb|true| \\
 
   131     \indexml{goals\_limit}\verb|goals_limit: int ref| & default \verb|10| \\
 
   129     \indexdef{}{ML}{goals\_limit}\verb|goals_limit: int ref| & default \verb|10| \\
 
   132     \indexml{Proof.show\_main\_goal}\verb|Proof.show_main_goal: bool ref| & default \verb|false| \\
 
   130     \indexdef{}{ML}{Proof.show\_main\_goal}\verb|Proof.show_main_goal: bool ref| & default \verb|false| \\
 
   133     \indexml{show\_hyps}\verb|show_hyps: bool ref| & default \verb|false| \\
 
   131     \indexdef{}{ML}{show\_hyps}\verb|show_hyps: bool ref| & default \verb|false| \\
 
   134     \indexml{show\_tags}\verb|show_tags: bool ref| & default \verb|false| \\
 
   132     \indexdef{}{ML}{show\_tags}\verb|show_tags: bool ref| & default \verb|false| \\
 
   135     \indexml{show\_question\_marks}\verb|show_question_marks: bool ref| & default \verb|true| \\
 
   133     \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool ref| & default \verb|true| \\
 
   136   \end{mldecls}
 
   134   \end{mldecls}
 
   137 
   135 
   138   These global ML variables control the detail of information that is
 
   136   These global ML variables control the detail of information that is
 
   139   displayed for types, terms, theorems, goals etc.
 
   137   displayed for types, terms, theorems, goals etc.
 
   140 
   138 
   231 }
 
   229 }
 
   232 \isamarkuptrue%
 
   230 \isamarkuptrue%
 
   233 %
 
   231 %
 
   234 \begin{isamarkuptext}%
 
   232 \begin{isamarkuptext}%
 
   235 \begin{mldecls}
 
   233 \begin{mldecls}
 
   236     \indexml{Pretty.setdepth}\verb|Pretty.setdepth: int -> unit| \\
 
   234     \indexdef{}{ML}{Pretty.setdepth}\verb|Pretty.setdepth: int -> unit| \\
 
   237     \indexml{Pretty.setmargin}\verb|Pretty.setmargin: int -> unit| \\
 
   235     \indexdef{}{ML}{Pretty.setmargin}\verb|Pretty.setmargin: int -> unit| \\
 
   238     \indexml{print\_depth}\verb|print_depth: int -> unit| \\
 
   236     \indexdef{}{ML}{print\_depth}\verb|print_depth: int -> unit| \\
 
   239   \end{mldecls}
 
   237   \end{mldecls}
 
   240 
   238 
   241   These ML functions set limits for pretty printed text.
 
   239   These ML functions set limits for pretty printed text.
 
   242 
   240 
   243   \begin{description}
 
   241   \begin{description}
 
   390     \indexdef{}{command}{notation}\hypertarget{command.notation}{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
 
   388     \indexdef{}{command}{notation}\hypertarget{command.notation}{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
 
   391     \indexdef{}{command}{no\_notation}\hypertarget{command.no-notation}{\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
 
   389     \indexdef{}{command}{no\_notation}\hypertarget{command.no-notation}{\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
 
   392   \end{matharray}
 
   390   \end{matharray}
 
   393 
   391 
   394   \begin{rail}
 
   392   \begin{rail}
 
   395     ('notation' | 'no\_notation') target? mode? (nameref structmixfix + 'and')
 
   393     ('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and')
 
   396     ;
 
   394     ;
 
   397   \end{rail}
 
   395   \end{rail}
 
   398 
   396 
   399   \begin{description}
 
   397   \begin{description}
 
   400 
   398 
   549 
   547 
   550   \indexdef{inner}{syntax}{type}\hypertarget{syntax.inner.type}{\hyperlink{syntax.inner.type}{\mbox{\isa{type}}}} & = & \verb|(| \isa{type} \verb|)| \\
 
   548   \indexdef{inner}{syntax}{type}\hypertarget{syntax.inner.type}{\hyperlink{syntax.inner.type}{\mbox{\isa{type}}}} & = & \verb|(| \isa{type} \verb|)| \\
 
   551     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}tid\ \ {\isacharbar}\ \ tvar\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_| \\
 
   549     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}tid\ \ {\isacharbar}\ \ tvar\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_| \\
 
   552     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}tid{\isachardoublequote}} \verb|::| \isa{{\isachardoublequote}sort\ \ {\isacharbar}\ \ tvar\ \ {\isachardoublequote}}\verb|::| \isa{{\isachardoublequote}sort\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_| \verb|::| \isa{{\isachardoublequote}sort{\isachardoublequote}} \\
 
   550     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}tid{\isachardoublequote}} \verb|::| \isa{{\isachardoublequote}sort\ \ {\isacharbar}\ \ tvar\ \ {\isachardoublequote}}\verb|::| \isa{{\isachardoublequote}sort\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_| \verb|::| \isa{{\isachardoublequote}sort{\isachardoublequote}} \\
 
   553     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ id\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|(| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|)| \isa{id} \\
 
   551     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ id\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|(| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|)| \isa{id} \\
 
   554     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}longid\ \ {\isacharbar}\ \ type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ longid\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|(| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|)| \isa{longid} \\
 
   552     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}longid\ \ {\isacharbar}\ \ type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ longid{\isachardoublequote}} \\
 
       
   553     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|(| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|)| \isa{longid} \\
 
   555     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|=>| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\
 
   554     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|=>| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\
 
   556     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \isa{{\isachardoublequote}{\isasymRightarrow}{\isachardoublequote}} \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\
 
   555     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \isa{{\isachardoublequote}{\isasymRightarrow}{\isachardoublequote}} \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\
 
   557     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|[| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|]| \verb|=>| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\
 
   556     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|[| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|]| \verb|=>| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\
 
   558     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|[| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|]| \isa{{\isachardoublequote}{\isasymRightarrow}{\isachardoublequote}} \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\\\
 
   557     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|[| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|]| \isa{{\isachardoublequote}{\isasymRightarrow}{\isachardoublequote}} \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\\\
 
   559 
   558 
   560   \indexdef{inner}{syntax}{sort}\hypertarget{syntax.inner.sort}{\hyperlink{syntax.inner.sort}{\mbox{\isa{sort}}}} & = & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ longid\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|{}|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|{| \isa{{\isachardoublequote}{\isacharparenleft}id\ {\isacharbar}\ longid{\isacharparenright}{\isachardoublequote}} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{{\isachardoublequote}{\isacharparenleft}id\ {\isacharbar}\ longid{\isacharparenright}{\isachardoublequote}} \verb|}| \\
 
   559   \indexdef{inner}{syntax}{sort}\hypertarget{syntax.inner.sort}{\hyperlink{syntax.inner.sort}{\mbox{\isa{sort}}}} & = & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ longid\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|{}| \\
 
       
   560     & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|{| \isa{{\isachardoublequote}{\isacharparenleft}id\ {\isacharbar}\ longid{\isacharparenright}{\isachardoublequote}} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{{\isachardoublequote}{\isacharparenleft}id\ {\isacharbar}\ longid{\isacharparenright}{\isachardoublequote}} \verb|}| \\
 
   561   \end{supertabular}
 
   561   \end{supertabular}
 
   562   \end{center}
 
   562   \end{center}
 
   563 
   563 
   564   \medskip Here literal terminals are printed \verb|verbatim|;
 
   564   \medskip Here literal terminals are printed \verb|verbatim|;
 
   565   see also \secref{sec:inner-lex} for further token categories of the
 
   565   see also \secref{sec:inner-lex} for further token categories of the
wneuper/isa