Hi Christian,
> To come back to the subject, I'm missing "iteration" of predicates,
> i.e., what "_^^n" is on relations but for predicates ("'a => 'a =>
> bool").this has been added in http://isabelle.in.tum.de/testboard/Isabelle/rev/69cee87927f0 – you can transfer theorems from the set relations in an ad-hoc using [to_pred]. You can also prove theorems for pred relations by means of … by (fact … [to_pred]), as has been done in many places of theory Relation. This could also be a contribution to the Isabelle theories for the next release. > PS: I suggest to rename "rel_comp" into "relcomp" (to be consistent with > "relpow"). This would also mean to rename the corresponding lemmas, although I would also appreciate consistency. Also the »pred_comp« abbreviation should be dropped, with the subsequent consequences for theorem names. This would also be something you could contribute if you like. > In @{theory Relation} there is a typo in the lemma name > "prod_comp_bot1". Fixed, thanks a lot. Cheers, 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
