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