[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
Here's a minimal example:
locale l = fixes x assumes "x = x"
interpretation l "Suc 0"
(* ?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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and