[isabelle] How to "unhide" constants in Isabelle



Dear Isabelle experts,

I am using constants such as Real.Real, Real.cauchy and Real.vanishes in my theory. However, as some implementation details of reals are hidden by the statement

    hide_const (open) vanishes cauchy positive Real

in "Real.thy", I have to use "Real.cauchy" instead of "cauchy" in my files, which is slightly annoying. Is there a way to "unhide" those constants in my files to make it more convenient?

Many thanks,
Wenda

--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge




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