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

[Lars Noschinski]

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