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/CCL/CCL.thy
changeset 80914 d97fdabd9e2b
parent 74563 042041c0ebeb
child 80917 2a77bc3b4eac 
--- a/src/CCL/CCL.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/CCL/CCL.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -27,18 +27,18 @@
 
 consts
   (*** Evaluation Judgement ***)
-  Eval      ::       "[i,i]\<Rightarrow>prop"          (infixl "\<longlongrightarrow>" 20)
+  Eval      ::       "[i,i]\<Rightarrow>prop"          (infixl \<open>\<longlongrightarrow>\<close> 20)
 
   (*** Bisimulations for pre-order and equality ***)
-  po          ::       "['a,'a]\<Rightarrow>o"           (infixl "[=" 50)
+  po          ::       "['a,'a]\<Rightarrow>o"           (infixl \<open>[=\<close> 50)
 
   (*** Term Formers ***)
   true        ::       "i"
   false       ::       "i"
-  pair        ::       "[i,i]\<Rightarrow>i"             ("(1<_,/_>)")
-  lambda      ::       "(i\<Rightarrow>i)\<Rightarrow>i"            (binder "lam " 55)
+  pair        ::       "[i,i]\<Rightarrow>i"             (\<open>(1<_,/_>)\<close>)
+  lambda      ::       "(i\<Rightarrow>i)\<Rightarrow>i"            (binder \<open>lam \<close> 55)
   "case"      ::       "[i,i,i,[i,i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
-  "apply"     ::       "[i,i]\<Rightarrow>i"             (infixl "`" 56)
+  "apply"     ::       "[i,i]\<Rightarrow>i"             (infixl \<open>`\<close> 56)
   bot         ::       "i"
 
   (******* EVALUATION SEMANTICS *******)
isabelle