tuned header
authorhaftmann
Mon Dec 10 11:24:14 2007 +0100 (2007-12-10 ago)
changeset 25596ad9e3594f3f3
parent 25595 6c48275f9c76
child 25597 34860182b250
tuned header
src/HOL/NumberTheory/IntPrimes.thy
src/HOL/Real/HahnBanach/Bounds.thy
     1.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Mon Dec 10 11:24:12 2007 +0100
     1.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Mon Dec 10 11:24:14 2007 +0100
     1.3 @@ -6,7 +6,9 @@
     1.4  
     1.5  header {* Divisibility and prime numbers (on integers) *}
     1.6  
     1.7 -theory IntPrimes imports Primes begin
     1.8 +theory IntPrimes
     1.9 +imports Primes
    1.10 +begin
    1.11  
    1.12  text {*
    1.13    The @{text dvd} relation, GCD, Euclid's extended algorithm, primes,
     2.1 --- a/src/HOL/Real/HahnBanach/Bounds.thy	Mon Dec 10 11:24:12 2007 +0100
     2.2 +++ b/src/HOL/Real/HahnBanach/Bounds.thy	Mon Dec 10 11:24:14 2007 +0100
     2.3 @@ -5,7 +5,9 @@
     2.4  
     2.5  header {* Bounds *}
     2.6  
     2.7 -theory Bounds imports Main Real begin
     2.8 +theory Bounds
     2.9 +imports Main Real
    2.10 +begin
    2.11  
    2.12  locale lub =
    2.13    fixes A and x