author haftmann Tue, 10 Jun 2008 15:30:59 +0200 changeset 27108 e447b3107696 parent 27107 4a7415c67063 child 27109 779e73b02cca
whitespace tuning
 src/HOL/Auth/Guard/GuardK.thy file | annotate | diff | comparison | revisions src/HOL/Complex/Fundamental_Theorem_Algebra.thy file | annotate | diff | comparison | revisions src/HOL/Hyperreal/Series.thy file | annotate | diff | comparison | revisions src/HOLCF/ex/Dnat.thy file | annotate | diff | comparison | revisions
```--- 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 @@

-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 @@

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 (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)
```