equal
deleted
inserted
replaced
507 qed |
507 qed |
508 |
508 |
509 |
509 |
510 subsection {* Class @{text finite} *} |
510 subsection {* Class @{text finite} *} |
511 |
511 |
512 setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*} |
|
513 class finite = |
512 class finite = |
514 assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)" |
513 assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)" |
515 setup {* Sign.parent_path *} |
|
516 hide_const finite |
|
517 |
|
518 context finite |
|
519 begin |
514 begin |
520 |
515 |
521 lemma finite [simp]: "finite (A \<Colon> 'a set)" |
516 lemma finite [simp]: "finite (A \<Colon> 'a set)" |
522 by (rule subset_UNIV finite_UNIV finite_subset)+ |
517 by (rule subset_UNIV finite_UNIV finite_subset)+ |
523 |
518 |