--- a/src/HOL/Finite.ML Fri Feb 18 20:25:29 2000 +0100
+++ b/src/HOL/Finite.ML Fri Feb 18 20:27:19 2000 +0100
@@ -170,6 +170,19 @@
bind_thm("finite_SigmaI", ballI RSN (2,result()));
Addsimps [finite_SigmaI];
+Goal "[| finite (UNIV::'a set); finite (UNIV::'b set)|] ==> finite (UNIV::('a * 'b) set)";
+by (subgoal_tac "(UNIV::('a * 'b) set) = Sigma UNIV (%x. UNIV)" 1);
+by (etac ssubst 1);
+by (etac finite_SigmaI 1);
+by Auto_tac;
+qed "finite_Prod_UNIV";
+
+Goal "finite (UNIV :: ('a::finite * 'b::finite) set)";
+br (finite_Prod_UNIV) 1;
+br finite 1;
+br finite 1;
+qed "finite_Prod";
+
(** The powerset of a finite set **)
Goal "finite(Pow A) ==> finite A";
--- a/src/HOL/WF_Rel.thy Fri Feb 18 20:25:29 2000 +0100
+++ b/src/HOL/WF_Rel.thy Fri Feb 18 20:27:19 2000 +0100
@@ -11,6 +11,10 @@
*)
WF_Rel = Finite +
+
+(* actually belongs to Finite.thy *)
+instance "*" :: (finite,finite) finite (finite_Prod)
+
consts
less_than :: "(nat*nat)set"
inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"