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".

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.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.