equal
deleted
inserted
replaced
18 | insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)" |
18 | insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)" |
19 |
19 |
20 use "Tools/set_comprehension_pointfree.ML" |
20 use "Tools/set_comprehension_pointfree.ML" |
21 |
21 |
22 simproc_setup finite_Collect ("finite (Collect P)") = |
22 simproc_setup finite_Collect ("finite (Collect P)") = |
23 {* Set_Comprehension_Pointfree.simproc *} |
23 {* K Set_Comprehension_Pointfree.simproc *} |
24 |
24 |
25 |
25 |
26 lemma finite_induct [case_names empty insert, induct set: finite]: |
26 lemma finite_induct [case_names empty insert, induct set: finite]: |
27 -- {* Discharging @{text "x \<notin> F"} entails extra work. *} |
27 -- {* Discharging @{text "x \<notin> F"} entails extra work. *} |
28 assumes "finite F" |
28 assumes "finite F" |