src/HOL/Finite_Set.thy
 changeset 24163 9e6a2a7da86a parent 23949 06a988643235 child 24194 96013f81faef
```     1.1 --- a/src/HOL/Finite_Set.thy	Tue Aug 07 09:38:44 2007 +0200
1.2 +++ b/src/HOL/Finite_Set.thy	Tue Aug 07 09:38:46 2007 +0200
1.3 @@ -7,7 +7,7 @@
1.4  header {* Finite sets *}
1.5
1.6  theory Finite_Set
1.7 -imports IntDef Divides
1.8 +imports IntDef Divides Option
1.9  begin
1.10
1.11  subsection {* Definition and basic properties *}
1.12 @@ -2687,18 +2687,14 @@
1.13  interpretation
1.14    Linorder ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <"]
1.15  where
1.16 -  "Linorder.Min (op \<le>) = Min" and "Linorder.Max (op \<le>) = Max"
1.17 +  "Linorder.Min (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = Min"
1.18 +  and "Linorder.Max (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = Max"
1.19  proof -
1.20    show "Linorder (op \<le> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> bool) op <"
1.21    by (rule Linorder.intro, rule linorder_axioms)
1.22 -  have "Linorder (op \<le> \<Colon> 'b \<Rightarrow> 'b \<Rightarrow> bool) op <"
1.23 -  by (rule Linorder.intro, rule linorder_axioms)
1.24 -  then interpret Linorder1: Linorder ["op \<le> \<Colon> 'b \<Rightarrow> 'b \<Rightarrow> bool" "op <"] .
1.25 -  show "Linorder1.Min = Min" by (simp add: Min_def Linorder1.Min_def ord_class.min)
1.26 -  have "Linorder (op \<le> \<Colon> 'c \<Rightarrow> 'c \<Rightarrow> bool) op <"
1.27 -  by (rule Linorder.intro, rule linorder_axioms)
1.28 -  then interpret Linorder2: Linorder ["op \<le> \<Colon> 'c \<Rightarrow> 'c \<Rightarrow> bool" "op <"] .
1.29 -  show "Linorder2.Max = Max" by (simp add: Max_def Linorder2.Max_def ord_class.max)
1.30 +  then interpret Linorder: Linorder ["op \<le> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> bool" "op <"] .
1.31 +  show "Linorder.Min = Min" by (simp add: Min_def Linorder.Min_def ord_class.min)
1.32 +  show "Linorder.Max = Max" by (simp add: Max_def Linorder.Max_def ord_class.max)
1.33  qed
1.34
1.35  interpretation
```