Re: [isabelle] Basic help with class and instantiation

Le Tue, 14 Aug 2012 01:29:22 +0200, Yannick Duchêne (Hibou57) <yannick_duchene at> 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.” [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.