# HG changeset patch
# User haftmann
# Date 1215076567 -7200
# Node ID eecd9d84e41b5451b0ebef37489b71cfe01d1e22
# Parent  5c1fb7d262bfc701bed886022d5dd02207d8fc38
added lemma antiquotation

diff -r 5c1fb7d262bf -r eecd9d84e41b doc-src/IsarRef/Thy/Document_Preparation.thy
--- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Thu Jul 03 11:16:05 2008 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Thu Jul 03 11:16:07 2008 +0200
@@ -135,6 +135,7 @@
   \begin{matharray}{rcl}
     @{antiquotation_def "theory"} & : & \isarantiq \\
     @{antiquotation_def "thm"} & : & \isarantiq \\
+    @{antiquotation_def "lemma"} & : & \isarantiq \\
     @{antiquotation_def "prop"} & : & \isarantiq \\
     @{antiquotation_def "term"} & : & \isarantiq \\
     @{antiquotation_def const} & : & \isarantiq \\
@@ -173,6 +174,7 @@
     antiquotation:
       'theory' options name |
       'thm' options thmrefs |
+      'lemma' options prop 'by' method |
       'prop' options prop |
       'term' options term |
       'const' options term |
@@ -216,6 +218,9 @@
   \item [@{text "@{prop \<phi>}"}] prints a well-typed proposition @{text
   "\<phi>"}.
 
+  \item [@{text "@{lemma \<phi> by m}"}] asserts a well-typed proposition @{text
+  "\<phi>"} to be provable by method @{text m} and prints @{text "\<phi>"}.
+
   \item [@{text "@{term t}"}] prints a well-typed term @{text "t"}.
 
   \item [@{text "@{const c}"}] prints a logical or syntactic constant
diff -r 5c1fb7d262bf -r eecd9d84e41b doc-src/IsarRef/Thy/document/Document_Preparation.tex
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Thu Jul 03 11:16:05 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Thu Jul 03 11:16:07 2008 +0200
@@ -151,6 +151,7 @@
 \begin{matharray}{rcl}
     \indexdef{}{antiquotation}{theory}\hypertarget{antiquotation.theory}{\hyperlink{antiquotation.theory}{\mbox{\isa{theory}}}} & : & \isarantiq \\
     \indexdef{}{antiquotation}{thm}\hypertarget{antiquotation.thm}{\hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}} & : & \isarantiq \\
+    \indexdef{}{antiquotation}{lemma}\hypertarget{antiquotation.lemma}{\hyperlink{antiquotation.lemma}{\mbox{\isa{lemma}}}} & : & \isarantiq \\
     \indexdef{}{antiquotation}{prop}\hypertarget{antiquotation.prop}{\hyperlink{antiquotation.prop}{\mbox{\isa{prop}}}} & : & \isarantiq \\
     \indexdef{}{antiquotation}{term}\hypertarget{antiquotation.term}{\hyperlink{antiquotation.term}{\mbox{\isa{term}}}} & : & \isarantiq \\
     \indexdef{}{antiquotation}{const}\hypertarget{antiquotation.const}{\hyperlink{antiquotation.const}{\mbox{\isa{const}}}} & : & \isarantiq \\
@@ -189,6 +190,7 @@
     antiquotation:
       'theory' options name |
       'thm' options thmrefs |
+      'lemma' options prop 'by' method |
       'prop' options prop |
       'term' options term |
       'const' options term |
@@ -230,6 +232,8 @@
 
   \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}prop\ {\isasymphi}{\isacharbraceright}{\isachardoublequote}}] prints a well-typed proposition \isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}.
 
+  \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}}.
+
   \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ t{\isacharbraceright}{\isachardoublequote}}] prints a well-typed term \isa{{\isachardoublequote}t{\isachardoublequote}}.
 
   \item [\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}const\ c{\isacharbraceright}{\isachardoublequote}}] prints a logical or syntactic constant