[isabelle] interpretation and sublocale add Pure.prop to ?thesis



Dear Isar experts,

In interpretation and sublocale statements, the generated abbreviation ?thesis contains an additional Pure.prop . Unfortunately, this marker renders ?thesis unusable for show statements.

Here's a minimal example:

locale l = fixes x assumes "x = x"
interpretation l "Suc 0"
proof -
  (* ?thesis here is "Pure.prop (HOL.Trueprop (l (Suc 0)))" *)
  show "PROP ?thesis"   (* does not work -> failed to refine any pending goal *)
  show "Trueprop (l (Suc 0))"  (* works *)

Why do interpretation and sublocale statements add this Pure.prop marker to ?thesis? And what is Pure.prop needed for at all?

Best,
Andreas




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