discontinued presumable workarounds for extra inter-theory space, which are obsolete since 0e5fa27d3293;
authorwenzelm
Tue Jul 22 14:52:35 2014 +0200 (2014-07-22)
changeset 576075ff0cf3f5f6f
parent 57606 6df377afda4a
child 57608 5d761f9292cf
discontinued presumable workarounds for extra inter-theory space, which are obsolete since 0e5fa27d3293;
src/Doc/Locales/Examples1.thy
src/Doc/Locales/Examples2.thy
src/Doc/Locales/Examples3.thy
     1.1 --- a/src/Doc/Locales/Examples1.thy	Tue Jul 22 14:36:31 2014 +0200
     1.2 +++ b/src/Doc/Locales/Examples1.thy	Tue Jul 22 14:52:35 2014 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  theory Examples1
     1.5  imports Examples
     1.6  begin
     1.7 -text {* \vspace{-5ex} *}
     1.8 +
     1.9  section {* Use of Locales in Theories and Proofs
    1.10    \label{sec:interpretation} *}
    1.11  
     2.1 --- a/src/Doc/Locales/Examples2.thy	Tue Jul 22 14:36:31 2014 +0200
     2.2 +++ b/src/Doc/Locales/Examples2.thy	Tue Jul 22 14:52:35 2014 +0200
     2.3 @@ -1,7 +1,6 @@
     2.4  theory Examples2
     2.5  imports Examples
     2.6  begin
     2.7 -text {* \vspace{-5ex} *}
     2.8    interpretation %visible int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool"
     2.9      where "int.less x y = (x < y)"
    2.10    proof -
     3.1 --- a/src/Doc/Locales/Examples3.thy	Tue Jul 22 14:36:31 2014 +0200
     3.2 +++ b/src/Doc/Locales/Examples3.thy	Tue Jul 22 14:52:35 2014 +0200
     3.3 @@ -1,7 +1,7 @@
     3.4  theory Examples3
     3.5  imports Examples
     3.6  begin
     3.7 -text {* \vspace{-5ex} *}
     3.8 +
     3.9  subsection {* Third Version: Local Interpretation
    3.10    \label{sec:local-interpretation} *}
    3.11