[isabelle] Issue with typeclass-parsing: div-class cannot be specified



Hi all,

Refering to Isabelle2012 and also the current development version
(Changeset: eb7b59cc8e08)

I just found the following issue with type-class parsing:

term "a::'a::div"

*** Inner syntax error (line 5 of
"/home/lammich/devel/isabelle/Scratch.thy") at "div"
*** Failed to parse term


The same occurs for 
  fixes a :: "'a::div"

and also for variations of the syntax like: "'a::{div}" or
"'a::{times,div}"


It seems to be the case that term-syntax influences sort syntax here:
  Adding a no_notation "div" (infixl "div" 70) solves the problem.

Term-syntax also influences type syntax, so 
  typedecl div
  term "a::div"
has a simlar problem.


If this "feature" of interfering term and sort syntax is intended, I
propose renaming the div-typeclass, such that a user can again refer to
it without nasty no_notation or whatever workarounds.


--
  Peter







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