# HG changeset patch
# User wenzelm
# Date 1406033555 -7200
# Node ID 5ff0cf3f5f6f7b3b35aa3f2a7505450ac89d103b
# Parent  6df377afda4ad2c7af114734aaa115ddd3b377de
discontinued presumable workarounds for extra inter-theory space, which are obsolete since 0e5fa27d3293;

diff -r 6df377afda4a -r 5ff0cf3f5f6f src/Doc/Locales/Examples1.thy
--- a/src/Doc/Locales/Examples1.thy	Tue Jul 22 14:36:31 2014 +0200
+++ b/src/Doc/Locales/Examples1.thy	Tue Jul 22 14:52:35 2014 +0200
@@ -1,7 +1,7 @@
 theory Examples1
 imports Examples
 begin
-text {* \vspace{-5ex} *}
+
 section {* Use of Locales in Theories and Proofs
   \label{sec:interpretation} *}
 
diff -r 6df377afda4a -r 5ff0cf3f5f6f src/Doc/Locales/Examples2.thy
--- a/src/Doc/Locales/Examples2.thy	Tue Jul 22 14:36:31 2014 +0200
+++ b/src/Doc/Locales/Examples2.thy	Tue Jul 22 14:52:35 2014 +0200
@@ -1,7 +1,6 @@
 theory Examples2
 imports Examples
 begin
-text {* \vspace{-5ex} *}
   interpretation %visible int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool"
     where "int.less x y = (x < y)"
   proof -
diff -r 6df377afda4a -r 5ff0cf3f5f6f src/Doc/Locales/Examples3.thy
--- a/src/Doc/Locales/Examples3.thy	Tue Jul 22 14:36:31 2014 +0200
+++ b/src/Doc/Locales/Examples3.thy	Tue Jul 22 14:52:35 2014 +0200
@@ -1,7 +1,7 @@
 theory Examples3
 imports Examples
 begin
-text {* \vspace{-5ex} *}
+
 subsection {* Third Version: Local Interpretation
   \label{sec:local-interpretation} *}