Re: [isabelle] Basic help with class and instantiation
Le Tue, 14 Aug 2012 01:29:22 +0200, Yannick Duchêne (Hibou57)
<yannick_duchene at yahoo.fr> a écrit:
P.S. By the way, what's the name of the default proof method Isabelle
uses in Instance Proof? Does not seems to be unfold_classes (as there is
an unfold_locales method) or any similar names I've tested.
At least, I've found an answer to this one. That's intro_classes; thus,
“instance proof” do the same as “instance proof intro_classes”.
“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