# HG changeset patch
# User wenzelm
# Date 1272311428 -7200
# Node ID 641a521bfc1953cfe91530aa15ce4f7507aff663
# Parent  5ab0f8859f9f32f6939e140e831f7cecb64f0d72
use 'example_proof' (invisible);

diff -r 5ab0f8859f9f -r 641a521bfc19 doc-src/IsarRef/Thy/Framework.thy
--- a/doc-src/IsarRef/Thy/Framework.thy	Mon Apr 26 21:45:08 2010 +0200
+++ b/doc-src/IsarRef/Thy/Framework.thy	Mon Apr 26 21:50:28 2010 +0200
@@ -79,8 +79,7 @@
 text_raw {*\medskip\begin{minipage}{0.6\textwidth}*}
 
 (*<*)
-lemma True
-proof
+example_proof
 (*>*)
     assume "x \<in> A" and "x \<in> B"
     then have "x \<in> A \<inter> B" ..
@@ -107,8 +106,7 @@
 *}
 
 (*<*)
-lemma True
-proof
+example_proof
 (*>*)
     assume "x \<in> A" and "x \<in> B"
     then have "x \<in> A \<inter> B" by (rule IntI)
@@ -130,8 +128,7 @@
 text_raw {*\medskip\begin{minipage}{0.6\textwidth}*}
 
 (*<*)
-lemma True
-proof
+example_proof
 (*>*)
     have "x \<in> \<Inter>\<A>"
     proof
@@ -178,8 +175,7 @@
 text_raw {*\medskip\begin{minipage}{0.6\textwidth}*}
 
 (*<*)
-lemma True
-proof
+example_proof
 (*>*)
     assume "x \<in> \<Union>\<A>"
     then have C
@@ -212,8 +208,7 @@
 *}
 
 (*<*)
-lemma True
-proof
+example_proof
 (*>*)
     assume "x \<in> \<Union>\<A>"
     then obtain A where "x \<in> A" and "A \<in> \<A>" ..
@@ -817,8 +812,7 @@
 *}
 
 text_raw {* \begingroup\footnotesize *}
-(*<*)lemma True
-proof
+(*<*)example_proof
 (*>*)
   txt_raw {* \begin{minipage}[t]{0.18\textwidth} *}
   have "A \<longrightarrow> B"
@@ -877,8 +871,7 @@
 text_raw {*\begin{minipage}{0.5\textwidth}*}
 
 (*<*)
-lemma True
-proof
+example_proof
 (*>*)
   have "\<And>x y. A x \<Longrightarrow> B y \<Longrightarrow> C x y"
   proof -
@@ -987,8 +980,7 @@
 *}
 
 (*<*)
-lemma True
-proof
+example_proof
 (*>*)
   have "a = b" sorry
   also have "\<dots> = c" sorry
diff -r 5ab0f8859f9f -r 641a521bfc19 doc-src/IsarRef/Thy/document/Framework.tex
--- a/doc-src/IsarRef/Thy/document/Framework.tex	Mon Apr 26 21:45:08 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Framework.tex	Mon Apr 26 21:50:28 2010 +0200
@@ -97,11 +97,11 @@
 \medskip\begin{minipage}{0.6\textwidth}
 %
 \isadelimproof
-%
+\ \ \ \ %
 \endisadelimproof
 %
 \isatagproof
-\ \ \ \ \isacommand{assume}\isamarkupfalse%
+\isacommand{assume}\isamarkupfalse%
 \ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}x\ {\isasymin}\ B{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{have}\isamarkupfalse%
@@ -135,11 +135,11 @@
 \isamarkuptrue%
 %
 \isadelimproof
-%
+\ \ \ \ %
 \endisadelimproof
 %
 \isatagproof
-\ \ \ \ \isacommand{assume}\isamarkupfalse%
+\isacommand{assume}\isamarkupfalse%
 \ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}x\ {\isasymin}\ B{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{have}\isamarkupfalse%
@@ -166,11 +166,11 @@
 \medskip\begin{minipage}{0.6\textwidth}
 %
 \isadelimproof
-%
+\ \ \ \ %
 \endisadelimproof
 %
 \isatagproof
-\ \ \ \ \isacommand{have}\isamarkupfalse%
+\isacommand{have}\isamarkupfalse%
 \ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymInter}{\isasymA}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{proof}\isamarkupfalse%
 \isanewline
@@ -198,9 +198,9 @@
 {\isafoldnoproof}%
 %
 \isadelimnoproof
-\isanewline
 %
 \endisadelimnoproof
+\isanewline
 %
 \isadelimproof
 \ \ \ \ %
@@ -251,11 +251,11 @@
 \medskip\begin{minipage}{0.6\textwidth}
 %
 \isadelimproof
-%
+\ \ \ \ %
 \endisadelimproof
 %
 \isatagproof
-\ \ \ \ \isacommand{assume}\isamarkupfalse%
+\isacommand{assume}\isamarkupfalse%
 \ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}{\isasymA}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{have}\isamarkupfalse%
@@ -286,9 +286,9 @@
 {\isafoldnoproof}%
 %
 \isadelimnoproof
-\isanewline
 %
 \endisadelimnoproof
+\isanewline
 %
 \isadelimproof
 \ \ \ \ %
@@ -326,11 +326,11 @@
 \isamarkuptrue%
 %
 \isadelimproof
-%
+\ \ \ \ %
 \endisadelimproof
 %
 \isatagproof
-\ \ \ \ \isacommand{assume}\isamarkupfalse%
+\isacommand{assume}\isamarkupfalse%
 \ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}{\isasymA}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{obtain}\isamarkupfalse%
@@ -1186,9 +1186,9 @@
 {\isafoldproof}%
 %
 \isadelimproof
-\isanewline
 %
 \endisadelimproof
+\isanewline
 %
 \isadelimnoproof
 \ \ \ \ \ \ %
@@ -1201,9 +1201,9 @@
 {\isafoldnoproof}%
 %
 \isadelimnoproof
-\isanewline
 %
 \endisadelimnoproof
+\isanewline
 %
 \isadelimproof
 \ \ %
@@ -1268,11 +1268,11 @@
 \begin{minipage}{0.5\textwidth}
 %
 \isadelimproof
-%
+\ \ %
 \endisadelimproof
 %
 \isatagproof
-\ \ \isacommand{have}\isamarkupfalse%
+\isacommand{have}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isasymAnd}x\ y{\isachardot}\ A\ x\ {\isasymLongrightarrow}\ B\ y\ {\isasymLongrightarrow}\ C\ x\ y{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{proof}\isamarkupfalse%
 \ {\isacharminus}\isanewline
@@ -1300,9 +1300,9 @@
 {\isafoldnoproof}%
 %
 \isadelimnoproof
-\isanewline
 %
 \endisadelimnoproof
+\isanewline
 %
 \isadelimproof
 \ \ %
@@ -1342,9 +1342,9 @@
 {\isafoldnoproof}%
 %
 \isadelimnoproof
-\isanewline
 %
 \endisadelimnoproof
+\isanewline
 %
 \isadelimproof
 \ \ %
@@ -1456,11 +1456,11 @@
 \isamarkuptrue%
 %
 \isadelimproof
-%
+\ \ %
 \endisadelimproof
 %
 \isatagproof
-\ \ \isacommand{have}\isamarkupfalse%
+\isacommand{have}\isamarkupfalse%
 \ {\isachardoublequoteopen}a\ {\isacharequal}\ b{\isachardoublequoteclose}\ \isacommand{sorry}\isamarkupfalse%
 \isanewline
 \ \ \isacommand{also}\isamarkupfalse%