Re: [isabelle] Question about Contexts and Sorts



Brian,

On Wed, 2011-01-19 at 10:08 -0800, Brian Huffman wrote:
> > lemma (in B) "b = c" by (simp only: B_class.b_def c_def)
> 
> I guess the confusion comes from the fact that in context "B", the
> term "b" can have two completely different meanings, depending on its
> type. I wonder if there is a way to configure the pretty-printer so
> that it would be easier to distinguish the two?

Indeed.  Try

  lemma (in B) "b = c"
  apply (cut_tac b_def)

(with Long Names switched on for greater effect).  No wonder I was
confused.

Thanks for your quick reply!

Kind regards,
Tjark






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