Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/String.thy
changeset 80760 be8c0e039a5e
parent 80088 5afbf04418ec
child 80932 261cd8722677 
--- a/src/HOL/String.thy	Sun Aug 25 12:43:43 2024 +0200
+++ b/src/HOL/String.thy	Sun Aug 25 15:02:19 2024 +0200
@@ -218,6 +218,8 @@
 syntax
   "_Char" :: "str_position \<Rightarrow> char"    ("CHR _")
   "_Char_ord" :: "num_const \<Rightarrow> char"   ("CHR _")
+syntax_consts
+  "_Char" "_Char_ord" \<rightleftharpoons> Char
 
 type_synonym string = "char list"
 
@@ -522,6 +524,8 @@
 syntax
   "_Literal" :: "str_position \<Rightarrow> String.literal"   ("STR _")
   "_Ascii" :: "num_const \<Rightarrow> String.literal"        ("STR _")
+syntax_consts
+  "_Literal" "_Ascii" \<rightleftharpoons> String.Literal
 
 ML_file \<open>Tools/literal.ML\<close>
isabelle