[isabelle-dev] Conversions between ('a * 'a) set and 'a => 'a => bool relations

[Florian Haftmann]

Hi Stefan,

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

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