Re: [isabelle] Isabelle2015-RC0 available for testing

[message continues (how do I email?)]

Another question: Sometimes I have some helper lemmas and at the end
of my theory I declare
hide_fact helper_lemma
to clean up the namespace.
Can I use the new private keyword to accomplish the same or is it only
considered for special cases when I already use context blocks?

Overall, RC0 looks very nice. Great job!


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