Re: [isabelle] Isabelle2015-RC0 available for testing



On Sun, 12 Apr 2015, C. Diekmann wrote:

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?

Yes, the 'private' keyword is exactly for this kind of application. The isar-ref manual adds this explanation:

  Neither a global @{command theory} nor a @{command locale} target
  provides a local scope by itself: an extra unnamed context is required
  to use @{keyword "private"} or @{keyword "qualified"} here.


	Makarius





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