[isabelle] syntax in auxiliary contexts
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] syntax in auxiliary contexts
- From: Christian Sternagel <c-sterna at jaist.ac.jp>
- Date: Wed, 13 Jun 2012 11:39:31 +0900
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:13.0) Gecko/20120605 Thunderbird/13.0
Why is the behavior after defining notation inside an auxiliary context
different depending on whether this auxiliary context is inside another
More specifically, consider
fixes P :: "'a => 'a => bool"
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and