# HG changeset patch
# User haftmann
# Date 1213104659 -7200
# Node ID e447b31076968f760aaeb43747b230586c232d21
# Parent  4a7415c670636e76dfb9525ccfebfad4fa5360e6
whitespace tuning

diff -r 4a7415c67063 -r e447b3107696 src/HOL/Auth/Guard/GuardK.thy
--- 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
diff -r 4a7415c67063 -r e447b3107696 src/HOL/Complex/Fundamental_Theorem_Algebra.thy
--- 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 *}
diff -r 4a7415c67063 -r e447b3107696 src/HOL/Hyperreal/Series.thy
--- 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
 
diff -r 4a7415c67063 -r e447b3107696 src/HOLCF/ex/Dnat.thy
--- 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)