[isabelle-dev] scala-2.12.2

Lars Hupel hupel at in.tum.de
Thu Jun 22 22:03:34 CEST 2017

> I took the opportunity to have a look at it and found out it can be done
> differently, see attached patch.

The patch is now running on testboard:

> The clue about "integer_of_char" is that it had to work regardless
> whether HOL chars are represented authentic or by target language
> characters (importing "~~/src/HOL/Library/Code_Char").
> Nowadays this can be achieved without spelling out the chars explicitly.
>  The last stone to turn around before had been the de-constructivation
> of the char type (b3f2b8c906a6).

Thanks for investigating this.


More information about the isabelle-dev mailing list