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/Statespace/StateSpaceSyntax.thy
changeset 80914 d97fdabd9e2b
parent 69597 ff784d5a5bfb 
--- a/src/HOL/Statespace/StateSpaceSyntax.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Statespace/StateSpaceSyntax.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -11,9 +11,9 @@
 can choose if you want to use it or not.\<close>
 
 syntax 
-  "_statespace_lookup" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"  ("_\<cdot>_" [60, 60] 60)
+  "_statespace_lookup" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"  (\<open>_\<cdot>_\<close> [60, 60] 60)
   "_statespace_update" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b)"
-  "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)"  ("_<_>" [900, 0] 900)
+  "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)"  (\<open>_<_>\<close> [900, 0] 900)
 
 translations
   "_statespace_updates f (_updbinds b bs)" ==
isabelle