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 yahoo.fr> a écrit:

Hello,

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.