--- 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
--- 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