--- a/doc-src/IsarRef/Thy/Framework.thy Wed Nov 10 20:43:22 2010 +0100
+++ b/doc-src/IsarRef/Thy/Framework.thy Thu Nov 11 13:07:41 2010 +0100
@@ -649,25 +649,25 @@
theorem True
proof
(*>*)
- txt_raw {* \begin{minipage}[t]{0.4\textwidth} *}
+ txt_raw {* \begin{minipage}[t]{0.45\textwidth} *}
{
fix x
have "B x" sorry %noproof
}
note `\<And>x. B x`
- txt_raw {* \end{minipage}\quad\begin{minipage}[t]{0.4\textwidth} *}(*<*)next(*>*)
+ txt_raw {* \end{minipage}\quad\begin{minipage}[t]{0.45\textwidth} *}(*<*)next(*>*)
{
assume A
have B sorry %noproof
}
note `A \<Longrightarrow> B`
- txt_raw {* \end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth} *}(*<*)next(*>*)
+ txt_raw {* \end{minipage}\\[3ex]\begin{minipage}[t]{0.45\textwidth} *}(*<*)next(*>*)
{
def x \<equiv> a
have "B x" sorry %noproof
}
note `B a`
- txt_raw {* \end{minipage}\quad\begin{minipage}[t]{0.4\textwidth} *}(*<*)next(*>*)
+ txt_raw {* \end{minipage}\quad\begin{minipage}[t]{0.45\textwidth} *}(*<*)next(*>*)
{
obtain x where "A x" sorry %noproof
have B sorry %noproof
--- a/doc-src/IsarRef/Thy/document/Framework.tex Wed Nov 10 20:43:22 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Framework.tex Thu Nov 11 13:07:41 2010 +0100
@@ -758,7 +758,7 @@
%
\isatagproof
%
-\begin{minipage}[t]{0.4\textwidth}
+\begin{minipage}[t]{0.45\textwidth}
\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
@@ -796,7 +796,7 @@
\isanewline
\ \ \isacommand{note}\isamarkupfalse%
\ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{60}{\isacharbackquoteclose}}%
-\end{minipage}\quad\begin{minipage}[t]{0.4\textwidth}
+\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}
\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
@@ -834,7 +834,7 @@
\isanewline
\ \ \isacommand{note}\isamarkupfalse%
\ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{60}{\isacharbackquoteclose}}%
-\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}
+\end{minipage}\\[3ex]\begin{minipage}[t]{0.45\textwidth}
\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{def}\isamarkupfalse%
@@ -872,7 +872,7 @@
\isanewline
\ \ \isacommand{note}\isamarkupfalse%
\ {\isaliteral{60}{\isacharbackquoteopen}}B\ a{\isaliteral{60}{\isacharbackquoteclose}}%
-\end{minipage}\quad\begin{minipage}[t]{0.4\textwidth}
+\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}
\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{obtain}\isamarkupfalse%