# HG changeset patch
# User wenzelm
# Date 1234716469 -3600
# Node ID 0ecdefc17d9a447b440a55de2de15260091b5f33
# Parent  05d5615e12d33384e29efdf5e9d132240b82de81
tuned;

diff -r 05d5615e12d3 -r 0ecdefc17d9a doc-src/IsarRef/Thy/Framework.thy
--- a/doc-src/IsarRef/Thy/Framework.thy	Sat Feb 14 22:58:30 2009 +0100
+++ b/doc-src/IsarRef/Thy/Framework.thy	Sun Feb 15 17:47:49 2009 +0100
@@ -606,7 +606,7 @@
   The most interesting derived context element in Isar is @{command
   obtain} \cite[\S5.3]{Wenzel-PhD}, which supports generalized
   elimination steps in a purely forward manner.  The @{command obtain}
-  element takes a specification of parameters @{text "\<^vec>x"} and
+  command takes a specification of parameters @{text "\<^vec>x"} and
   assumptions @{text "\<^vec>A"} to be added to the context, together
   with a proof of a case rule stating that this extension is
   conservative (i.e.\ may be removed from closed results later on):
@@ -647,8 +647,7 @@
   \medskip The subsequent Isar proof texts explain all context
   elements introduced above using the formal proof language itself.
   After finishing a local proof within a block, we indicate the
-  exported result via @{command note}.  This illustrates the meaning
-  of Isar context elements without goals getting in between.
+  exported result via @{command note}.
 *}
 
 (*<*)
@@ -684,6 +683,10 @@
 qed
 (*>*)
 
+text {*
+  \bigskip\noindent This illustrates the meaning of Isar context
+  elements without goals getting in between.
+*}
 
 subsection {* Structured statements \label{sec:framework-stmt} *}