[isabelle-dev] Mixfix-Syntax not recognized

[Makarius]

On Tue, 6 Aug 2013, René Neumann wrote:

> I'm currently on revision 8d8cb75ab20a

> begin
> definition foo :: "'a list ⇒ nat" ("(_⇧ω)") where
> "foo xs = length xs"

> It works with Isabelle-2013, but already failed ~100 revisions ago in
> -dev (unfortunately forgot to write the exact revision down).
>
> It is probably related to the thread "Subscripts within identifiers",
> but I'm not definitly sure.

This thread is still pending, and it needs to converge to some conclusion 
soon, one that is relevant for the next official release.

When you are "on" some Isabelle repository version you need to cope with 
the ups and downs of what is happening there: frequent updates, knowing 
the changeset id for later discussion about it.

The repository is not a place to get "latest stuff", and "rolling updates" 
are not compatible with the Isabelle release quality standards.  Instead, 
the repository is the place where work on the system and its libries 
happens.


 	Makarius