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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
