equal
deleted
inserted
replaced
506 qed |
506 qed |
507 qed |
507 qed |
508 |
508 |
509 instance bool :: finite proof |
509 instance bool :: finite proof |
510 qed (simp add: UNIV_bool) |
510 qed (simp add: UNIV_bool) |
|
511 |
|
512 instance set :: (finite) finite |
|
513 by default (simp only: Pow_UNIV [symmetric] finite_Pow_iff finite) |
511 |
514 |
512 instance unit :: finite proof |
515 instance unit :: finite proof |
513 qed (simp add: UNIV_unit) |
516 qed (simp add: UNIV_unit) |
514 |
517 |
515 instance sum :: (finite, finite) finite proof |
518 instance sum :: (finite, finite) finite proof |