[isabelle-dev] cs. 3911cf09899a

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Mon Oct 3 16:59:37 CEST 2011

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

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

Our current efforts for having 'a set as type constrcutor will turn this
superfluous if not hindering.




PGP available:

-------------- 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>

More information about the isabelle-dev mailing list