[isabelle] Undefined facts in skip_proofs mode



Hello,

Cornelius and I noticed an oddity when using the system option
"skip_proofs". Consider this simple proof:

lemma "(xs::'a list) = xs"
proof (induct xs)
  case Cons
  thm Cons.hyps
  from Cons show ?case by auto
qed auto

Notice the "thm" command in the middle. Without "skip_proofs", this goes
through fine. Enabling "skip_proofs" produces this message:

*** Undefined fact: "Cons.hyps" (line 8 of
"~/tmp/Skip_Proof/Skip_Proof.thy")
*** At command "thm" (line 8 of "~/tmp/Skip_Proof/Skip_Proof.thy")

I have attached a session demonstrating the difference. Run with

$ isabelle build -d . -v Skip_Proof

Reproducible in all official releases since 2013-2.

Cheers
Lars

Attachment: skip_proofs.zip
Description: Zip compressed data



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