| changeset 9351 | 5d53e3f35152 |
| parent 9338 | fcf7f29a3447 |
| child 9399 | effc8d44c89c |
--- 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";