doc-src/IsarRef/Thy/document/Document_Preparation.tex
changeset 27453 eecd9d84e41b
parent 27054 f1ef0973d0a8
child 27881 f0d543629376
     1.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Thu Jul 03 11:16:05 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Thu Jul 03 11:16:07 2008 +0200
     1.3 @@ -151,6 +151,7 @@
     1.4  \begin{matharray}{rcl}
     1.5      \indexdef{}{antiquotation}{theory}\hypertarget{antiquotation.theory}{\hyperlink{antiquotation.theory}{\mbox{\isa{theory}}}} & : & \isarantiq \\
     1.6      \indexdef{}{antiquotation}{thm}\hypertarget{antiquotation.thm}{\hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}} & : & \isarantiq \\
     1.7 +    \indexdef{}{antiquotation}{lemma}\hypertarget{antiquotation.lemma}{\hyperlink{antiquotation.lemma}{\mbox{\isa{lemma}}}} & : & \isarantiq \\
     1.8      \indexdef{}{antiquotation}{prop}\hypertarget{antiquotation.prop}{\hyperlink{antiquotation.prop}{\mbox{\isa{prop}}}} & : & \isarantiq \\
     1.9      \indexdef{}{antiquotation}{term}\hypertarget{antiquotation.term}{\hyperlink{antiquotation.term}{\mbox{\isa{term}}}} & : & \isarantiq \\
    1.10      \indexdef{}{antiquotation}{const}\hypertarget{antiquotation.const}{\hyperlink{antiquotation.const}{\mbox{\isa{const}}}} & : & \isarantiq \\
    1.11 @@ -189,6 +190,7 @@
    1.12      antiquotation:
    1.13        'theory' options name |
    1.14        'thm' options thmrefs |
    1.15 +      'lemma' options prop 'by' method |
    1.16        'prop' options prop |
    1.17        'term' options term |
    1.18        'const' options term |
    1.19 @@ -230,6 +232,8 @@
    1.20  
    1.21    \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prop\ {\isasymphi}{\isacharbraceright}{\isachardoublequote}}] prints a well-typed proposition \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}.
    1.22  
    1.23 +  \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}lemma\ {\isasymphi}\ by\ m{\isacharbraceright}{\isachardoublequote}}] asserts a well-typed proposition \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}} to be provable by method \isa{m} and prints \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}.
    1.24 +
    1.25    \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ t{\isacharbraceright}{\isachardoublequote}}] prints a well-typed term \isa{{\isachardoublequote}t{\isachardoublequote}}.
    1.26  
    1.27    \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}const\ c{\isacharbraceright}{\isachardoublequote}}] prints a logical or syntactic constant