Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned header
authorhaftmann
Mon, 10 Dec 2007 11:24:14 +0100
changeset 25596 ad9e3594f3f3
parent 25595 6c48275f9c76
child 25597 34860182b250
tuned header
src/HOL/NumberTheory/IntPrimes.thy file | annotate | diff | comparison | revisions
src/HOL/Real/HahnBanach/Bounds.thy file | annotate | diff | comparison | revisions 
--- 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,
--- 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
isabelle