Re: [isabelle] Operator clash for $

On 16/06/16 12:08, Andreas Lochbihler wrote:
> Hi Manuel,
> The $ notation is used also in other places of the HOL Library, e.g., in
> Library/FinFun_Syntax and HOLCF/Cfun. I'd recommend that the operations
> by default use subscripts for disambiguation, e.g. (we can discuss about
> the concrete subscripts),
>   op $\<^sub>v for vectors
>   op $\<^sup>p for formal power series
>   op $\<^sup>f for FinFun

(This thread still seems to be unresolved.)

How about this?

  $ for vectors
  $\<^sup>p for formal power series
  $\<^sup>f for FinFun

> Then, if a user wants to use several of the theories at the same time,
> she can always use unambiguous syntax. However, typing subscripts can
> be annoying

How about this in etc/abbrevs?

"$" = "$\<^sub>f"
"$" = "$\<^sub>p"


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