# HG changeset patch
# User wenzelm
# Date 963773615 -7200
# Node ID 8b09c29453acf9d9fe8cd9bacd505701026c2302
# Parent  82e8b18e698514a209caa286550da265439096f7
instance unit :: finite;

diff -r 82e8b18e6985 -r 8b09c29453ac src/HOL/WF_Rel.thy
--- a/src/HOL/WF_Rel.thy	Sun Jul 16 20:53:19 2000 +0200
+++ b/src/HOL/WF_Rel.thy	Sun Jul 16 20:53:35 2000 +0200
@@ -13,7 +13,9 @@
 WF_Rel = Finite +
 
 (* actually belongs to Finite.thy *)
-instance "*" :: (finite,finite) finite   (finite_Prod) 
+instance unit :: finite                  (finite_unit)
+instance "*" :: (finite,finite) finite   (finite_Prod)
+
 
 consts
   less_than :: "(nat*nat)set"