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

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


	Makarius


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