Re: [isabelle] Replacing COMP
On Wed, 31 Jul 2013, René Neumann wrote:
I'm with Tobias (as he stated in the thread you mentioned) to have an OF
and/or THEN variant which allows to instantiate the premise without
handling ==> and !! in a special way, because it is sometimes extremely
Tools that really need that (which was not yet proven here) are doing that
via the "prop" protective marker, and protectI, protectD rules etc.
together with plain resolution of Pure.
This is how all the second-generation locale infrastructure was made in
the early/mid 2000-nds (COMP is from the early 1990-ies).
This archive was generated by a fusion of
Pipermail (Mailman edition) and