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 80932 261cd8722677
parent 80760 be8c0e039a5e
child 81113 6fefd6c602fa 
--- a/src/HOL/String.thy	Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/String.thy	Mon Sep 23 13:32:38 2024 +0200
@@ -216,15 +216,15 @@
   by (cases c) simp
 
 syntax
-  "_Char" :: "str_position \<Rightarrow> char"    ("CHR _")
-  "_Char_ord" :: "num_const \<Rightarrow> char"   ("CHR _")
+  "_Char" :: "str_position \<Rightarrow> char"    (\<open>CHR _\<close>)
+  "_Char_ord" :: "num_const \<Rightarrow> char"   (\<open>CHR _\<close>)
 syntax_consts
   "_Char" "_Char_ord" \<rightleftharpoons> Char
 
 type_synonym string = "char list"
 
 syntax
-  "_String" :: "str_position \<Rightarrow> string"    ("_")
+  "_String" :: "str_position \<Rightarrow> string"    (\<open>_\<close>)
 
 ML_file \<open>Tools/string_syntax.ML\<close>
 
@@ -522,8 +522,8 @@
 code_datatype "0 :: String.literal" String.Literal
 
 syntax
-  "_Literal" :: "str_position \<Rightarrow> String.literal"   ("STR _")
-  "_Ascii" :: "num_const \<Rightarrow> String.literal"        ("STR _")
+  "_Literal" :: "str_position \<Rightarrow> String.literal"   (\<open>STR _\<close>)
+  "_Ascii" :: "num_const \<Rightarrow> String.literal"        (\<open>STR _\<close>)
 syntax_consts
   "_Literal" "_Ascii" \<rightleftharpoons> String.Literal
isabelle