Re: [isabelle] Undefined facts in skip_proofs mode
On Mon, 28 Jul 2014, Lars Hupel wrote:
Cornelius and I noticed an oddity when using the system option
skip_proofs is one of many add-on features that try to address certain
situations, without telling what that was years ago or what it might be
today. The doc-strings say "skip over proofs (implicit 'sorry')" in
Isabelle/Scala or "Skip over proofs" in Proof.
So what did have have in mind when using it? It might explain the
confusion. Or it might lead to new insight which general principles may
supersede skip_proofs at some point -- and absorb similar or different
features in the usual manner.
This archive was generated by a fusion of
Pipermail (Mailman edition) and