Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] "HOL-Library.Code_Char" replacement

Email Gateway (Aug 22 2022 at 19:12):

From: Mohammad Abdulaziz <mohammad.abdulaziz8@gmail.com>
Hi Everyone,

In an older project I have, I used to import the theory
"HOL-Library.Code_Char" for generating sml code that uses the type
"char". Now it seems that this theory can no longer be imported. Is
there an alternative to it?

Mohammad

Email Gateway (Aug 22 2022 at 19:12):

From: Makarius <makarius@sketis.net>
The NEWS file has this entry for Isabelle2018:

• Clarified relationship of characters, strings and code generation:

  • Type "char" is now a proper datatype of 8-bit values.

[...]

- Theory HOL-Library.Code_Char is gone; study the explanations
concerning "String.literal" in the tutorial on code generation to
get an idea how target-language string literals can be converted to
HOL string values and vice versa.

Both the NEWS and the codegen tutorial are accessible in the
Isabelle/jEdit Documentation panel.

Makarius

Last updated: Nov 21 2024 at 12:39 UTC