equal
deleted
inserted
replaced
511 |
511 |
512 setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*} |
512 setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*} |
513 class finite = |
513 class finite = |
514 assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)" |
514 assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)" |
515 setup {* Sign.parent_path *} |
515 setup {* Sign.parent_path *} |
516 hide const finite |
516 hide_const finite |
517 |
517 |
518 context finite |
518 context finite |
519 begin |
519 begin |
520 |
520 |
521 lemma finite [simp]: "finite (A \<Colon> 'a set)" |
521 lemma finite [simp]: "finite (A \<Colon> 'a set)" |