Re: [isabelle] Replacing COMP

Am 31.07.2013 22:58, schrieb Makarius:
> 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.

I'm not an Isabelle-Dev. I'm not interested in writing tools, I just
want to prove theorems.

René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift

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