[isabelle-dev] interpretation command: "show ?thesis" causes type error

Brian Huffman brianh at cs.pdx.edu
Tue Oct 5 21:07:28 CEST 2010

When proving a lemma, the term abbreviation ?thesis typically has type
"bool", and saying "show ?thesis" usually works.

But with "interpretation", it doesn't work. Here is a toy example that
shows what I mean:

locale foo = fixes x :: "'a::type" assumes x: "x = x"

term "foo" (* it has type 'a => bool, as expected. *)

interpretation myfoo: foo True
proof -
  term ?thesis  (* "foo True" :: prop *)
  show ?thesis

*** Type unification failed: Clash of types "prop" and "bool"
*** Type error in application: incompatible operand type
*** Operator:  Trueprop :: bool => prop
*** Operand:   PROP ?thesis :: prop
*** At command "show"

I am using revision 1410c84013b9, but the same error occurs with the
last few release versions as well.

- Brian

More information about the isabelle-dev mailing list