# HG changeset patch
# User haftmann
# Date 1197282254 -3600
# Node ID ad9e3594f3f3637000700d07c6bce7c833e9de0c
# Parent  6c48275f9c7612a47554a6e867984f028960ba4e
tuned header

diff -r 6c48275f9c76 -r ad9e3594f3f3 src/HOL/NumberTheory/IntPrimes.thy
--- a/src/HOL/NumberTheory/IntPrimes.thy	Mon Dec 10 11:24:12 2007 +0100
+++ b/src/HOL/NumberTheory/IntPrimes.thy	Mon Dec 10 11:24:14 2007 +0100
@@ -6,7 +6,9 @@
 
 header {* Divisibility and prime numbers (on integers) *}
 
-theory IntPrimes imports Primes begin
+theory IntPrimes
+imports Primes
+begin
 
 text {*
   The @{text dvd} relation, GCD, Euclid's extended algorithm, primes,
diff -r 6c48275f9c76 -r ad9e3594f3f3 src/HOL/Real/HahnBanach/Bounds.thy
--- a/src/HOL/Real/HahnBanach/Bounds.thy	Mon Dec 10 11:24:12 2007 +0100
+++ b/src/HOL/Real/HahnBanach/Bounds.thy	Mon Dec 10 11:24:14 2007 +0100
@@ -5,7 +5,9 @@
 
 header {* Bounds *}
 
-theory Bounds imports Main Real begin
+theory Bounds
+imports Main Real
+begin
 
 locale lub =
   fixes A and x