Re: [isabelle] Hide all constructors of a datatype automatically

Le Sat, 14 Dec 2013 13:27:01 +0100, Yannick Duchêne (Hibou57) <yannick_duchene at> a écrit:


May a solution can be found somewhere in “implementation.pdf”, from the documentation pan. I believe it's possible to modify a theory context using an embedded SML function (embedded in the theory file), without a need for modifying Isabelle internal (I'm looking at it, will be back if I feel I've found anything useful in “implementation.pdf”).

May be looking at page 10 and later, “0.2 SML embedded into Isabelle/Isar”, then at page 59 and later, “2.1 Types”.

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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