[isabelle-dev] cs. 3911cf09899a

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20111003/fee94977/attachment.asc>