[isabelle] Private/qualified in locales



Dear list,

is there any shorter way than that to hide a fact in a locale?


context constructors begin
context begin (* two contexts for private qualifier *)

  private lemma seval_correct0:
    ...

end
end



Cheers
Lars




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