--- a/NEWS Tue Apr 24 22:22:25 2018 +0100
+++ b/NEWS Wed Apr 25 09:04:25 2018 +0000
@@ -210,7 +210,7 @@
* Type "String.literal" (for code generation) is now isomorphic
to lists of 7-bit (ASCII) values; concrete values can be written
as "STR ''...''" for sequences of printable characters and
- "ASCII 0x..." for one single ASCII code point given
+ "STR 0x..." for one single ASCII code point given
as hexadecimal numeral.
* Type "String.literal" supports concatenation "... + ..."
--- a/src/Doc/Codegen/Adaptation.thy Tue Apr 24 22:22:25 2018 +0100
+++ b/src/Doc/Codegen/Adaptation.thy Wed Apr 25 09:04:25 2018 +0000
@@ -174,7 +174,7 @@
Literal values of type @{typ String.literal} can be written
as @{text "STR ''\<dots>''"} for sequences of printable characters and
- @{text "ASCII 0x\<dots>"} for one single ASCII code point given
+ @{text "STR 0x\<dots>"} for one single ASCII code point given
as hexadecimal numeral; @{typ String.literal} supports concatenation
@{text "\<dots> + \<dots>"} for all standard target languages.
--- a/src/HOL/Library/Code_Test.thy Tue Apr 24 22:22:25 2018 +0100
+++ b/src/HOL/Library/Code_Test.thy Wed Apr 25 09:04:25 2018 +0000
@@ -84,8 +84,8 @@
definition list where "list f xs = map (node \<circ> f) xs"
-definition X :: yxml_of_term where "X = yot_literal (ASCII 0x05)"
-definition Y :: yxml_of_term where "Y = yot_literal (ASCII 0x06)"
+definition X :: yxml_of_term where "X = yot_literal (STR 0x05)"
+definition Y :: yxml_of_term where "Y = yot_literal (STR 0x06)"
definition XY :: yxml_of_term where "XY = yot_append X Y"
definition XYX :: yxml_of_term where "XYX = yot_append XY X"
--- a/src/HOL/String.thy Tue Apr 24 22:22:25 2018 +0100
+++ b/src/HOL/String.thy Wed Apr 25 09:04:25 2018 +0000
@@ -119,7 +119,7 @@
lemma char_of_nat [simp]:
"char_of (of_nat n) = char_of n"
by (simp add: char_of_def String.char_of_def drop_bit_of_nat)
-
+
end
lemma inj_on_char_of_nat [simp]:
@@ -407,7 +407,7 @@
\<^enum> Printable text as string prefixed with @{text STR};
- \<^enum> A single ascii value as numerical value prefixed with @{text ASCII}.
+ \<^enum> A single ascii value as numerical hexadecimal value prefixed with @{text STR}.
\<close>
instantiation String.literal :: zero
@@ -455,8 +455,8 @@
code_datatype "0 :: String.literal" String.Literal
syntax
- "_Ascii" :: "num_const \<Rightarrow> String.literal" ("ASCII _")
"_Literal" :: "str_position \<Rightarrow> String.literal" ("STR _")
+ "_Ascii" :: "num_const \<Rightarrow> String.literal" ("STR _")
ML_file "Tools/literal.ML"