whitespace tuning
authorhaftmann
Tue Jun 10 15:30:59 2008 +0200 (2008-06-10)
changeset 27108e447b3107696
parent 27107 4a7415c67063
child 27109 779e73b02cca
whitespace tuning
src/HOL/Auth/Guard/GuardK.thy
src/HOL/Complex/Fundamental_Theorem_Algebra.thy
src/HOL/Hyperreal/Series.thy
src/HOLCF/ex/Dnat.thy
     1.1 --- a/src/HOL/Auth/Guard/GuardK.thy	Tue Jun 10 15:30:58 2008 +0200
     1.2 +++ b/src/HOL/Auth/Guard/GuardK.thy	Tue Jun 10 15:30:59 2008 +0200
     1.3 @@ -16,7 +16,9 @@
     1.4  
     1.5  header{*protocol-independent confidentiality theorem on keys*}
     1.6  
     1.7 -theory GuardK imports Analz Extensions begin
     1.8 +theory GuardK
     1.9 +imports Analz Extensions
    1.10 +begin
    1.11  
    1.12  (******************************************************************************
    1.13  messages where all the occurrences of Key n are
     2.1 --- a/src/HOL/Complex/Fundamental_Theorem_Algebra.thy	Tue Jun 10 15:30:58 2008 +0200
     2.2 +++ b/src/HOL/Complex/Fundamental_Theorem_Algebra.thy	Tue Jun 10 15:30:59 2008 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  header{*Fundamental Theorem of Algebra*}
     2.5  
     2.6  theory Fundamental_Theorem_Algebra
     2.7 -  imports  Univ_Poly Dense_Linear_Order Complex
     2.8 +imports Univ_Poly Dense_Linear_Order Complex
     2.9  begin
    2.10  
    2.11  section {* Square root of complex numbers *}
     3.1 --- a/src/HOL/Hyperreal/Series.thy	Tue Jun 10 15:30:58 2008 +0200
     3.2 +++ b/src/HOL/Hyperreal/Series.thy	Tue Jun 10 15:30:59 2008 +0200
     3.3 @@ -541,7 +541,7 @@
     3.4  apply (simp add: mult_ac)
     3.5  apply (rule_tac x = "norm (f N) * (1/ (1 - c)) / (c ^ N)" in exI)
     3.6  apply (rule sums_divide) 
     3.7 -apply (rule sums_mult) 
     3.8 +apply (rule sums_mult)
     3.9  apply (auto intro!: geometric_sums)
    3.10  done
    3.11  
     4.1 --- a/src/HOLCF/ex/Dnat.thy	Tue Jun 10 15:30:58 2008 +0200
     4.2 +++ b/src/HOLCF/ex/Dnat.thy	Tue Jun 10 15:30:59 2008 +0200
     4.3 @@ -5,7 +5,9 @@
     4.4  Theory for the domain of natural numbers  dnat = one ++ dnat
     4.5  *)
     4.6  
     4.7 -theory Dnat imports HOLCF begin
     4.8 +theory Dnat
     4.9 +imports HOLCF
    4.10 +begin
    4.11  
    4.12  domain dnat = dzero | dsucc (dpred :: dnat)
    4.13