1.1 --- a/doc-src/IsarRef/Thy/Framework.thy	Mon Apr 26 21:45:08 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Framework.thy	Mon Apr 26 21:50:28 2010 +0200
     1.3 @@ -79,8 +79,7 @@
     1.4  text_raw {*\medskip\begin{minipage}{0.6\textwidth}*}
     1.5  
     1.6  (*<*)
     1.7 -lemma True
     1.8 -proof
     1.9 +example_proof
    1.10  (*>*)
    1.11      assume "x \<in> A" and "x \<in> B"
    1.12      then have "x \<in> A \<inter> B" ..
    1.13 @@ -107,8 +106,7 @@
    1.14  *}
    1.15  
    1.16  (*<*)
    1.17 -lemma True
    1.18 -proof
    1.19 +example_proof
    1.20  (*>*)
    1.21      assume "x \<in> A" and "x \<in> B"
    1.22      then have "x \<in> A \<inter> B" by (rule IntI)
    1.23 @@ -130,8 +128,7 @@
    1.24  text_raw {*\medskip\begin{minipage}{0.6\textwidth}*}
    1.25  
    1.26  (*<*)
    1.27 -lemma True
    1.28 -proof
    1.29 +example_proof
    1.30  (*>*)
    1.31      have "x \<in> \<Inter>\<A>"
    1.32      proof
    1.33 @@ -178,8 +175,7 @@
    1.34  text_raw {*\medskip\begin{minipage}{0.6\textwidth}*}
    1.35  
    1.36  (*<*)
    1.37 -lemma True
    1.38 -proof
    1.39 +example_proof
    1.40  (*>*)
    1.41      assume "x \<in> \<Union>\<A>"
    1.42      then have C
    1.43 @@ -212,8 +208,7 @@
    1.44  *}
    1.45  
    1.46  (*<*)
    1.47 -lemma True
    1.48 -proof
    1.49 +example_proof
    1.50  (*>*)
    1.51      assume "x \<in> \<Union>\<A>"
    1.52      then obtain A where "x \<in> A" and "A \<in> \<A>" ..
    1.53 @@ -817,8 +812,7 @@
    1.54  *}
    1.55  
    1.56  text_raw {* \begingroup\footnotesize *}
    1.57 -(*<*)lemma True
    1.58 -proof
    1.59 +(*<*)example_proof
    1.60  (*>*)
    1.61    txt_raw {* \begin{minipage}[t]{0.18\textwidth} *}
    1.62    have "A \<longrightarrow> B"
    1.63 @@ -877,8 +871,7 @@
    1.64  text_raw {*\begin{minipage}{0.5\textwidth}*}
    1.65  
    1.66  (*<*)
    1.67 -lemma True
    1.68 -proof
    1.69 +example_proof
    1.70  (*>*)
    1.71    have "\<And>x y. A x \<Longrightarrow> B y \<Longrightarrow> C x y"
    1.72    proof -
    1.73 @@ -987,8 +980,7 @@
    1.74  *}
    1.75  
    1.76  (*<*)
    1.77 -lemma True
    1.78 -proof
    1.79 +example_proof
    1.80  (*>*)
    1.81    have "a = b" sorry
    1.82    also have "\<dots> = c" sorry

     2.1 --- a/doc-src/IsarRef/Thy/document/Framework.tex	Mon Apr 26 21:45:08 2010 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/Framework.tex	Mon Apr 26 21:50:28 2010 +0200
     2.3 @@ -97,11 +97,11 @@
     2.4  \medskip\begin{minipage}{0.6\textwidth}
     2.5  %
     2.6  \isadelimproof
     2.7 -%
     2.8 +\ \ \ \ %
     2.9  \endisadelimproof
    2.10  %
    2.11  \isatagproof
    2.12 -\ \ \ \ \isacommand{assume}\isamarkupfalse%
    2.13 +\isacommand{assume}\isamarkupfalse%
    2.14  \ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}x\ {\isasymin}\ B{\isachardoublequoteclose}\isanewline
    2.15  \ \ \ \ \isacommand{then}\isamarkupfalse%
    2.16  \ \isacommand{have}\isamarkupfalse%
    2.17 @@ -135,11 +135,11 @@
    2.18  \isamarkuptrue%
    2.19  %
    2.20  \isadelimproof
    2.21 -%
    2.22 +\ \ \ \ %
    2.23  \endisadelimproof
    2.24  %
    2.25  \isatagproof
    2.26 -\ \ \ \ \isacommand{assume}\isamarkupfalse%
    2.27 +\isacommand{assume}\isamarkupfalse%
    2.28  \ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}x\ {\isasymin}\ B{\isachardoublequoteclose}\isanewline
    2.29  \ \ \ \ \isacommand{then}\isamarkupfalse%
    2.30  \ \isacommand{have}\isamarkupfalse%
    2.31 @@ -166,11 +166,11 @@
    2.32  \medskip\begin{minipage}{0.6\textwidth}
    2.33  %
    2.34  \isadelimproof
    2.35 -%
    2.36 +\ \ \ \ %
    2.37  \endisadelimproof
    2.38  %
    2.39  \isatagproof
    2.40 -\ \ \ \ \isacommand{have}\isamarkupfalse%
    2.41 +\isacommand{have}\isamarkupfalse%
    2.42  \ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymInter}{\isasymA}{\isachardoublequoteclose}\isanewline
    2.43  \ \ \ \ \isacommand{proof}\isamarkupfalse%
    2.44  \isanewline
    2.45 @@ -198,9 +198,9 @@
    2.46  {\isafoldnoproof}%
    2.47  %
    2.48  \isadelimnoproof
    2.49 -\isanewline
    2.50  %
    2.51  \endisadelimnoproof
    2.52 +\isanewline
    2.53  %
    2.54  \isadelimproof
    2.55  \ \ \ \ %
    2.56 @@ -251,11 +251,11 @@
    2.57  \medskip\begin{minipage}{0.6\textwidth}
    2.58  %
    2.59  \isadelimproof
    2.60 -%
    2.61 +\ \ \ \ %
    2.62  \endisadelimproof
    2.63  %
    2.64  \isatagproof
    2.65 -\ \ \ \ \isacommand{assume}\isamarkupfalse%
    2.66 +\isacommand{assume}\isamarkupfalse%
    2.67  \ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}{\isasymA}{\isachardoublequoteclose}\isanewline
    2.68  \ \ \ \ \isacommand{then}\isamarkupfalse%
    2.69  \ \isacommand{have}\isamarkupfalse%
    2.70 @@ -286,9 +286,9 @@
    2.71  {\isafoldnoproof}%
    2.72  %
    2.73  \isadelimnoproof
    2.74 -\isanewline
    2.75  %
    2.76  \endisadelimnoproof
    2.77 +\isanewline
    2.78  %
    2.79  \isadelimproof
    2.80  \ \ \ \ %
    2.81 @@ -326,11 +326,11 @@
    2.82  \isamarkuptrue%
    2.83  %
    2.84  \isadelimproof
    2.85 -%
    2.86 +\ \ \ \ %
    2.87  \endisadelimproof
    2.88  %
    2.89  \isatagproof
    2.90 -\ \ \ \ \isacommand{assume}\isamarkupfalse%
    2.91 +\isacommand{assume}\isamarkupfalse%
    2.92  \ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}{\isasymA}{\isachardoublequoteclose}\isanewline
    2.93  \ \ \ \ \isacommand{then}\isamarkupfalse%
    2.94  \ \isacommand{obtain}\isamarkupfalse%
    2.95 @@ -1186,9 +1186,9 @@
    2.96  {\isafoldproof}%
    2.97  %
    2.98  \isadelimproof
    2.99 -\isanewline
   2.100  %
   2.101  \endisadelimproof
   2.102 +\isanewline
   2.103  %
   2.104  \isadelimnoproof
   2.105  \ \ \ \ \ \ %
   2.106 @@ -1201,9 +1201,9 @@
   2.107  {\isafoldnoproof}%
   2.108  %
   2.109  \isadelimnoproof
   2.110 -\isanewline
   2.111  %
   2.112  \endisadelimnoproof
   2.113 +\isanewline
   2.114  %
   2.115  \isadelimproof
   2.116  \ \ %
   2.117 @@ -1268,11 +1268,11 @@
   2.118  \begin{minipage}{0.5\textwidth}
   2.119  %
   2.120  \isadelimproof
   2.121 -%
   2.122 +\ \ %
   2.123  \endisadelimproof
   2.124  %
   2.125  \isatagproof
   2.126 -\ \ \isacommand{have}\isamarkupfalse%
   2.127 +\isacommand{have}\isamarkupfalse%
   2.128  \ {\isachardoublequoteopen}{\isasymAnd}x\ y{\isachardot}\ A\ x\ {\isasymLongrightarrow}\ B\ y\ {\isasymLongrightarrow}\ C\ x\ y{\isachardoublequoteclose}\isanewline
   2.129  \ \ \isacommand{proof}\isamarkupfalse%
   2.130  \ {\isacharminus}\isanewline
   2.131 @@ -1300,9 +1300,9 @@
   2.132  {\isafoldnoproof}%
   2.133  %
   2.134  \isadelimnoproof
   2.135 -\isanewline
   2.136  %
   2.137  \endisadelimnoproof
   2.138 +\isanewline
   2.139  %
   2.140  \isadelimproof
   2.141  \ \ %
   2.142 @@ -1342,9 +1342,9 @@
   2.143  {\isafoldnoproof}%
   2.144  %
   2.145  \isadelimnoproof
   2.146 -\isanewline
   2.147  %
   2.148  \endisadelimnoproof
   2.149 +\isanewline
   2.150  %
   2.151  \isadelimproof
   2.152  \ \ %
   2.153 @@ -1456,11 +1456,11 @@
   2.154  \isamarkuptrue%
   2.155  %
   2.156  \isadelimproof
   2.157 -%
   2.158 +\ \ %
   2.159  \endisadelimproof
   2.160  %
   2.161  \isatagproof
   2.162 -\ \ \isacommand{have}\isamarkupfalse%
   2.163 +\isacommand{have}\isamarkupfalse%
   2.164  \ {\isachardoublequoteopen}a\ {\isacharequal}\ b{\isachardoublequoteclose}\ \isacommand{sorry}\isamarkupfalse%
   2.165  \isanewline
   2.166  \ \ \isacommand{also}\isamarkupfalse%