Re: [isabelle] Hiding type class syntax



Nevermind, no_notation is what I want.

On Fri, Oct 27, 2017 at 11:07 AM Simon Wimmer <wimmersimon at gmail.com> wrote:

> Dear list,
>
> is there a way to hide syntax stemming from type classes?
> In particular, I want to remove the syntax for infinity from Extended_Nat.
> I tried
>
> no_syntax infinity :: "'a"  ("â") and
> no_syntax infinity :: "'a :: infinity"  ("â"),
>
> but to no avail.
>
> Simon
>



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