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

2012-03-04 Thread Florian Haftmann
Hi all, recently I did some work to setup Stefan's ancient pred_set_conv utility for relation predicates like sym(p) etc., see http://isabelle.in.tum.de/reports/Isabelle/file/tip/src/HOL/Relation.thy A few couple of things then came to surface: * Naming: »inductive_set foo« yields »foop« as the

Re: [isabelle-dev] [isabelle] Status of HOL/Import

2012-03-04 Thread Cezary Kaliszyk
Hi Florian, On Sun, Mar 04, 2012 at 10:15:38AM +0100, Florian Haftmann wrote: I've been working on the Importer stuff, not very deeply, but separating HOL4 and HOL Light contents, stripping generic parts of any name reference to HOL4, etc. [...] Great! There could be done a lot more on the

Re: [isabelle-dev] [isabelle] Status of HOL/Import

2012-03-04 Thread Florian Haftmann
but I would suggest waiting a week or two for the new import and trying to get the maps correct there. Ack. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital

Re: [isabelle-dev] [isabelle] Status of HOL/Import

2012-03-04 Thread Makarius
On Sun, 4 Mar 2012, Cezary Kaliszyk wrote: Makarius once suggested an antiquotation, that does something like 'print_theorems'. I have not investigated how to implement one? Pretty printing into latex source is not a big deal, if you are satisfied with regular multiline output in the display

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

2012-03-04 Thread Stefan Berghofer
Florian Haftmann wrote: * This is mainly a question to Stefan: there are some theorems commented out (e.g. »thm sym_INTER [to_pred]«) on which pred_set_conv chokes. I guess this is due to a higher-order situation, but I would be reassuring if you can confirm that. Hi Florian, this looks

Re: [isabelle-dev] Towards the next release

2012-03-04 Thread Thomas Sewell
We have a somewhat useful tool for expanding word equalities/inequalities bitwise, based on a part of some work Sascha and I did back in 2010. I've been meaning to push it up to the distribution for years, this will probably be a good time. The main reason I'm telling you this is that I'm now