On 09.03.2012 07:56, Florian Haftmann wrote:
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).
I am currently working on the CANDIDATEs marked as simp/intro/elim/...,
but have so far avoided those marked pred_set_conv (and code), as I
don't know yet what the effect of these attributes is.
Is there somewhere some documentation w.r.t to_set/to_pred/pred_set_conv?
-- Lars
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
