1.1 --- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Thu Jul 03 11:16:05 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Thu Jul 03 11:16:07 2008 +0200
     1.3 @@ -135,6 +135,7 @@
     1.4    \begin{matharray}{rcl}
     1.5      @{antiquotation_def "theory"} & : & \isarantiq \\
     1.6      @{antiquotation_def "thm"} & : & \isarantiq \\
     1.7 +    @{antiquotation_def "lemma"} & : & \isarantiq \\
     1.8      @{antiquotation_def "prop"} & : & \isarantiq \\
     1.9      @{antiquotation_def "term"} & : & \isarantiq \\
    1.10      @{antiquotation_def const} & : & \isarantiq \\
    1.11 @@ -173,6 +174,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 @@ -216,6 +218,9 @@
    1.20    \item [@{text "@{prop \<phi>}"}] prints a well-typed proposition @{text
    1.21    "\<phi>"}.
    1.22  
    1.23 +  \item [@{text "@{lemma \<phi> by m}"}] asserts a well-typed proposition @{text
    1.24 +  "\<phi>"} to be provable by method @{text m} and prints @{text "\<phi>"}.
    1.25 +
    1.26    \item [@{text "@{term t}"}] prints a well-typed term @{text "t"}.
    1.27  
    1.28    \item [@{text "@{const c}"}] prints a logical or syntactic constant

     2.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Thu Jul 03 11:16:05 2008 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Thu Jul 03 11:16:07 2008 +0200
     2.3 @@ -151,6 +151,7 @@
     2.4  \begin{matharray}{rcl}
     2.5      \indexdef{}{antiquotation}{theory}\hypertarget{antiquotation.theory}{\hyperlink{antiquotation.theory}{\mbox{\isa{theory}}}} & : & \isarantiq \\
     2.6      \indexdef{}{antiquotation}{thm}\hypertarget{antiquotation.thm}{\hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}} & : & \isarantiq \\
     2.7 +    \indexdef{}{antiquotation}{lemma}\hypertarget{antiquotation.lemma}{\hyperlink{antiquotation.lemma}{\mbox{\isa{lemma}}}} & : & \isarantiq \\
     2.8      \indexdef{}{antiquotation}{prop}\hypertarget{antiquotation.prop}{\hyperlink{antiquotation.prop}{\mbox{\isa{prop}}}} & : & \isarantiq \\
     2.9      \indexdef{}{antiquotation}{term}\hypertarget{antiquotation.term}{\hyperlink{antiquotation.term}{\mbox{\isa{term}}}} & : & \isarantiq \\
    2.10      \indexdef{}{antiquotation}{const}\hypertarget{antiquotation.const}{\hyperlink{antiquotation.const}{\mbox{\isa{const}}}} & : & \isarantiq \\
    2.11 @@ -189,6 +190,7 @@
    2.12      antiquotation:
    2.13        'theory' options name |
    2.14        'thm' options thmrefs |
    2.15 +      'lemma' options prop 'by' method |
    2.16        'prop' options prop |
    2.17        'term' options term |
    2.18        'const' options term |
    2.19 @@ -230,6 +232,8 @@
    2.20  
    2.21    \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prop\ {\isasymphi}{\isacharbraceright}{\isachardoublequote}}] prints a well-typed proposition \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}.
    2.22  
    2.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}}.
    2.24 +
    2.25    \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ t{\isacharbraceright}{\isachardoublequote}}] prints a well-typed term \isa{{\isachardoublequote}t{\isachardoublequote}}.
    2.26  
    2.27    \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}const\ c{\isacharbraceright}{\isachardoublequote}}] prints a logical or syntactic constant