# HG changeset patch
# User oheimb
# Date 950902039 -3600
# Node ID 08ad0a986db2c82280ea38add702035f229a9ba4
# Parent  e4726ac0863a40501aaa98f9f955080d43328931
added instance declaration for finite product

diff -r e4726ac0863a -r 08ad0a986db2 src/HOL/Finite.ML
--- 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";
diff -r e4726ac0863a -r 08ad0a986db2 src/HOL/WF_Rel.thy
--- 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"