author wenzelm Thu, 11 Nov 2010 13:07:41 +0100 changeset 40476 515eab39b6c2 parent 40475 8a57ff2c2600 child 40477 780c27276593
reduced danger of line breaks within minipage;
--- 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
{
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
{
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}}%
\ \ \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}}%
\ \ \ \ \isacommand{obtain}\isamarkupfalse%