# HG changeset patch
# User wenzelm
# Date 1289477261 -3600
# Node ID 515eab39b6c2807a15fe4e3e8d150bc431d160ad
# Parent  8a57ff2c2600904715b39d53db27bf20bf6d7c25
reduced danger of line breaks within minipage;

diff -r 8a57ff2c2600 -r 515eab39b6c2 doc-src/IsarRef/Thy/Framework.thy
--- 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
diff -r 8a57ff2c2600 -r 515eab39b6c2 doc-src/IsarRef/Thy/document/Framework.tex
--- 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%