Hi Lukas,
> +text {* Definitions could be moved to Transitive_Closure if they are
of more general use. *}
is there any striking reason *not* to do so in the first place? At a
first glimpse I can't see anything which relates to Enum.thy in those
theorems.
In my opinion it is high time to abandone the tradition of such comment
jokes in the HOL theories: if theorems are there, they *will* be used,
or at least it is not at our judgment for whom they are useful. So it
is best to have the theorems where they belong to, unless bootstrap
reasons dictate something else.
> +subsection {* An executable card operator on finite types *}
> +
> +lemma
> + [code]: "card R = length (filter R enum)"
> +by (simp add: distinct_length_filter[OF enum_distinct] enum_UNIV
Collect_def)
Our current efforts for having 'a set as type constrcutor will turn this
superfluous if not hindering.
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
