# HG changeset patch
# User haftmann
# Date 1191823466 -7200
# Node ID 5471709833a42a116ab8285dcb2ff11e7c183df3
# Parent  08865bb8709817ca234e7e66bcb7adf12eab51e6
clarified

diff -r 08865bb87098 -r 5471709833a4 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Oct 08 07:38:13 2007 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Oct 08 08:04:26 2007 +0200
@@ -2622,11 +2622,11 @@
 
 setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
 class finite (attach UNIV) = type +
-  assumes finite_UNIV: "finite UNIV"
+  assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
 setup {* Sign.parent_path *}
 hide const finite
 
-lemma finite [simp]: "finite (A::'a::finite set)"
+lemma finite [simp]: "finite (A \<Colon> 'a\<Colon>finite set)"
   by (rule finite_subset [OF subset_UNIV finite_UNIV])
 
 lemma univ_unit [noatp]:
@@ -2709,13 +2709,14 @@
 instance "fun" :: (finite, eq) eq ..
 
 lemma eq_fun [code func]:
-  "f = g \<longleftrightarrow> (\<forall>x\<Colon>'a\<Colon>finite \<in> UNIV. (f x \<Colon> 'b\<Colon>eq) = g x)"
+  fixes f g :: "'a\<Colon>finite \<Rightarrow> 'b\<Colon>eq"
+  shows "f = g \<longleftrightarrow> (\<forall>x\<in>UNIV. f x = g x)"
   unfolding expand_fun_eq by auto
 
 lemma order_fun [code func]:
-  "f \<le> g \<longleftrightarrow> (\<forall>x\<Colon>'a\<Colon>finite \<in> UNIV. (f x \<Colon> 'b\<Colon>order) \<le> g x)"
-  "f < g \<longleftrightarrow> f \<le> g \<and> (\<exists>x\<Colon>'a\<Colon>finite \<in> UNIV. (f x \<Colon> 'b\<Colon>order) < g x)"
-  unfolding le_fun_def less_fun_def less_le
-  by (auto simp add: expand_fun_eq)
+  fixes f g :: "'a\<Colon>finite \<Rightarrow> 'b\<Colon>order"
+  shows "f \<le> g \<longleftrightarrow> (\<forall>x\<in>UNIV. f x \<le> g x)"
+    and "f < g \<longleftrightarrow> f \<le> g \<and> (\<exists>x\<in>UNIV. f x \<noteq> g x)"
+  by (auto simp add: expand_fun_eq le_fun_def less_fun_def order_less_le)
 
 end