[isabelle-dev] Conversions between ('a * 'a) set and 'a => 'a => bool relations
florian.haftmann at informatik.tu-muenchen.de
Fri Mar 9 07:56:53 CET 2012
> I have fixed this bug now, see changeset b1d15637381a. Note that converting
> the above theorem (and the other theorems in Relation.thy marked with "FIXME")
> to predicate notation requires the generalized versions of theorems
> INF_INT_eq2 and SUP_UN_eq2, which should replace the more specific versions.
> Unfortunately, the Relation theory is currently a bit of a mess. Larger blocks
> of conversion lemmas are commented out for no good reason
well, the history is that I have not yet commented *in* them yet, just
marked them (among a couple of declarations) as CANDIDATE. So, anybody
who wants to go ahead can just comment in them and run the regular
regression (for which I do not expected any difficulties).
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev