1.1 --- a/src/HOL/Library/Continuity.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Library/Continuity.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -18,8 +18,8 @@
     1.4  "continuous F == !M. chain M \<longrightarrow> F(SUP i. M i) = (SUP i. F(M i))"
     1.5  
     1.6  abbreviation
     1.7 - bot :: "'a::order"
     1.8 -"bot == Sup {}"
     1.9 +  bot :: "'a::order" where
    1.10 +  "bot == Sup {}"
    1.11  
    1.12  lemma SUP_nat_conv:
    1.13   "(SUP n::nat. M n::'a::comp_lat) = join (M 0) (SUP n. M(Suc n))"
    1.14 @@ -91,7 +91,7 @@
    1.15  subsection "Chains"
    1.16  
    1.17  definition
    1.18 -  up_chain :: "(nat => 'a set) => bool"
    1.19 +  up_chain :: "(nat => 'a set) => bool" where
    1.20    "up_chain F = (\<forall>i. F i \<subseteq> F (Suc i))"
    1.21  
    1.22  lemma up_chainI: "(!!i. F i \<subseteq> F (Suc i)) ==> up_chain F"
    1.23 @@ -113,7 +113,7 @@
    1.24  
    1.25  
    1.26  definition
    1.27 -  down_chain :: "(nat => 'a set) => bool"
    1.28 +  down_chain :: "(nat => 'a set) => bool" where
    1.29    "down_chain F = (\<forall>i. F (Suc i) \<subseteq> F i)"
    1.30  
    1.31  lemma down_chainI: "(!!i. F (Suc i) \<subseteq> F i) ==> down_chain F"
    1.32 @@ -137,7 +137,7 @@
    1.33  subsection "Continuity"
    1.34  
    1.35  definition
    1.36 -  up_cont :: "('a set => 'a set) => bool"
    1.37 +  up_cont :: "('a set => 'a set) => bool" where
    1.38    "up_cont f = (\<forall>F. up_chain F --> f (\<Union>(range F)) = \<Union>(f ` range F))"
    1.39  
    1.40  lemma up_contI:
    1.41 @@ -164,7 +164,7 @@
    1.42  
    1.43  
    1.44  definition
    1.45 -  down_cont :: "('a set => 'a set) => bool"
    1.46 +  down_cont :: "('a set => 'a set) => bool" where
    1.47    "down_cont f =
    1.48      (\<forall>F. down_chain F --> f (Inter (range F)) = Inter (f ` range F))"
    1.49  
    1.50 @@ -194,7 +194,7 @@
    1.51  subsection "Iteration"
    1.52  
    1.53  definition
    1.54 -  up_iterate :: "('a set => 'a set) => nat => 'a set"
    1.55 +  up_iterate :: "('a set => 'a set) => nat => 'a set" where
    1.56    "up_iterate f n = (f^n) {}"
    1.57  
    1.58  lemma up_iterate_0 [simp]: "up_iterate f 0 = {}"
    1.59 @@ -246,7 +246,7 @@
    1.60  
    1.61  
    1.62  definition
    1.63 -  down_iterate :: "('a set => 'a set) => nat => 'a set"
    1.64 +  down_iterate :: "('a set => 'a set) => nat => 'a set" where
    1.65    "down_iterate f n = (f^n) UNIV"
    1.66  
    1.67  lemma down_iterate_0 [simp]: "down_iterate f 0 = UNIV"