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:
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.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and