# HG changeset patch
# User wenzelm
# Date 963773265 -7200
# Node ID 5d53e3f35152f500d910c61b91bdb237afe43905
# Parent  d855d9d1add94aaeb92a6e59221c5e56e094c6d8
added finite_unit;

diff -r d855d9d1add9 -r 5d53e3f35152 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Sun Jul 16 20:47:15 2000 +0200
+++ b/src/HOL/Finite.ML	Sun Jul 16 20:47:45 2000 +0200
@@ -186,6 +186,12 @@
 by (rtac finite 1);
 qed "finite_Prod";
 
+Goal "finite (UNIV :: unit set)";
+by (subgoal_tac "UNIV = {()}" 1);
+by (etac ssubst 1);
+by Auto_tac;
+qed "finite_unit";
+
 (** The powerset of a finite set **)
 
 Goal "finite(Pow A) ==> finite A";