> 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: <https://ci.isabelle.systems/jenkins/job/testboard/385/>. > 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. Cheers Lars _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
