--- a/src/HOL/Finite_Set.thy Sat Nov 14 18:37:49 2015 +0100
+++ b/src/HOL/Finite_Set.thy Sun Nov 15 12:39:51 2015 +0100
@@ -11,11 +11,17 @@
subsection \<open>Predicate for finite sets\<close>
+context
+ notes [[inductive_defs]]
+begin
+
inductive finite :: "'a set \<Rightarrow> bool"
where
emptyI [simp, intro!]: "finite {}"
| insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)"
+end
+
simproc_setup finite_Collect ("finite (Collect P)") = \<open>K Set_Comprehension_Pointfree.simproc\<close>
declare [[simproc del: finite_Collect]]