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
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
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
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
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
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
