| changeset 62093 | bd73a2279fcd |
| parent 61890 | f6ded81f5690 |
| child 62390 | 842917225d56 |
--- a/src/HOL/Finite_Set.thy Thu Jan 07 15:50:09 2016 +0100 +++ b/src/HOL/Finite_Set.thy Thu Jan 07 15:53:39 2016 +0100 @@ -12,7 +12,7 @@ subsection \<open>Predicate for finite sets\<close> context - notes [[inductive_defs]] + notes [[inductive_internals]] begin inductive finite :: "'a set \<Rightarrow> bool"