[isabelle] syntax in auxiliary contexts



Dear all,

Why is the behavior after defining notation inside an auxiliary context different depending on whether this auxiliary context is inside another context?

More specifically, consider

context
  fixes P :: "'a => 'a => bool"
begin

notation
  P ("\<^raw:\foo>")

term P

end

Here "term P" results in: "\<^raw:\foo>" (as expected)

However, as soon as I put the above code inside another context (named or unnamed), the syntax seems to be ignored and "term P" results in: "P".

What am I missing?

cheers

chris





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