--- a/src/HOL/Auth/Guard/GuardK.thy Tue Jun 10 15:30:58 2008 +0200
+++ b/src/HOL/Auth/Guard/GuardK.thy Tue Jun 10 15:30:59 2008 +0200
@@ -16,7 +16,9 @@
header{*protocol-independent confidentiality theorem on keys*}
-theory GuardK imports Analz Extensions begin
+theory GuardK
+imports Analz Extensions
+begin
(******************************************************************************
messages where all the occurrences of Key n are
--- a/src/HOL/Complex/Fundamental_Theorem_Algebra.thy Tue Jun 10 15:30:58 2008 +0200
+++ b/src/HOL/Complex/Fundamental_Theorem_Algebra.thy Tue Jun 10 15:30:59 2008 +0200
@@ -6,7 +6,7 @@
header{*Fundamental Theorem of Algebra*}
theory Fundamental_Theorem_Algebra
- imports Univ_Poly Dense_Linear_Order Complex
+imports Univ_Poly Dense_Linear_Order Complex
begin
section {* Square root of complex numbers *}
--- a/src/HOL/Hyperreal/Series.thy Tue Jun 10 15:30:58 2008 +0200
+++ b/src/HOL/Hyperreal/Series.thy Tue Jun 10 15:30:59 2008 +0200
@@ -541,7 +541,7 @@
apply (simp add: mult_ac)
apply (rule_tac x = "norm (f N) * (1/ (1 - c)) / (c ^ N)" in exI)
apply (rule sums_divide)
-apply (rule sums_mult)
+apply (rule sums_mult)
apply (auto intro!: geometric_sums)
done
--- a/src/HOLCF/ex/Dnat.thy Tue Jun 10 15:30:58 2008 +0200
+++ b/src/HOLCF/ex/Dnat.thy Tue Jun 10 15:30:59 2008 +0200
@@ -5,7 +5,9 @@
Theory for the domain of natural numbers dnat = one ++ dnat
*)
-theory Dnat imports HOLCF begin
+theory Dnat
+imports HOLCF
+begin
domain dnat = dzero | dsucc (dpred :: dnat)