equal
deleted
inserted
replaced
11 begin |
11 begin |
12 |
12 |
13 subsection {* Definition and basic properties *} |
13 subsection {* Definition and basic properties *} |
14 |
14 |
15 consts Finites :: "'a set set" |
15 consts Finites :: "'a set set" |
16 abbreviation (output) |
16 abbreviation |
17 "finite A = (A : Finites)" |
17 "finite A == A : Finites" |
18 |
18 |
19 inductive Finites |
19 inductive Finites |
20 intros |
20 intros |
21 emptyI [simp, intro!]: "{} : Finites" |
21 emptyI [simp, intro!]: "{} : Finites" |
22 insertI [simp, intro!]: "A : Finites ==> insert a A : Finites" |
22 insertI [simp, intro!]: "A : Finites ==> insert a A : Finites" |