Re: [isabelle] Question about Contexts and Sorts
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?
lemma (in B) "b = c"
apply (cut_tac b_def)
(with Long Names switched on for greater effect). No wonder I was
Thanks for your quick reply!
This archive was generated by a fusion of
Pipermail (Mailman edition) and