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/Sequents/ILL.thy
changeset 80917 2a77bc3b4eac
parent 80914 d97fdabd9e2b
child 80923 6c9628a116cc 
--- a/src/Sequents/ILL.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/Sequents/ILL.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -29,8 +29,8 @@
   PromAux :: "three_seqi"
 
 syntax
-  "_Trueprop" :: "single_seqe" (\<open>((_)/ \<turnstile> (_))\<close> [6,6] 5)
-  "_Context"  :: "two_seqe"   (\<open>((_)/ :=: (_))\<close> [6,6] 5)
+  "_Trueprop" :: "single_seqe" (\<open>(\<open>notation=\<open>infix Trueprop\<close>\<close>(_)/ \<turnstile> (_))\<close> [6,6] 5)
+  "_Context"  :: "two_seqe"   (\<open>(\<open>notation=\<open>infix Context\<close>\<close>(_)/ :=: (_))\<close> [6,6] 5)
   "_PromAux"  :: "three_seqe" (\<open>promaux {_||_||_}\<close>)
 
 parse_translation \<open>
isabelle