Re: [isabelle] antiquotations



-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Alexander Krauss wrote:
> Since bind_thms is impure, it can only update some global reference
> hanging around. This is incompatible with paralellism. At the moment it
> may work sometimes, but it is guaranteed to break sooner or later.

I'm curious about this: is it really the case that references are
inherently incompatible with parallelism? Is there some reason why it
cannot update a thread-local reference?

I would expect that you can cut the Isar/ML cake both ways:
anti-quotations in Isar or quotations in ML. I feel there should be a
confluence proof there somewhere :)

So, is there some reason this is not possible? In particular, Isar is
executed in ML, so it seems rather strange to me that you cannot
replicate it's effect in ML, for example by pasting the function calls
used by Isar into the ML.

cheers,
lucas
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFHs4HXogMqU4edHsMRAjj/AJ0fAFJEtuZYSsziwW/nTSJqqHNJsQCdFCyS
aOP6FBuIs/se0AyydGDCyqM=
=UlWW
-----END PGP SIGNATURE-----





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.