[isabelle-dev] NEWS: Revision of Big Operators on sets

[Florian Haftmann]

> Before this revision there we had the lemma Min.in_idem. What replaces
> this lemma?

By accident, this is now Min.subsumption.  I will revert this to
Min.in_idem ASAP.

The Big Operators material had became so entangled over the years (me
being not guiltless in that respect) that in large parts I did not
follow an inductive step-by-step approach for reform but rather used a
machete to get through.  Accidents like this then cannot be prevented in
all cases.

> My first try was making min an instance of folding_idem, but apparently
> the F in folding_idem is separate from the one in Min_def. So, what is
> the intended way to recover this lemma?
> 
>     interpret Min: folding_idem "min :: ('a :: {bot,linorder} ⇒ 'a ⇒
> 'a)" bot
>       by unfold_locales (simp_all add: fun_eq_iff min_max.inf.left_commute)

Big Operators on finite sets emerge from interpretation of locales in
Big_Operators.thy, cf. also NEWS.

Hope this helps,
	Florian

-- 

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: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130329/6eb7b8b0/attachment.sig>