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/Cube/Cube.thy
changeset 80923 6c9628a116cc
parent 80917 2a77bc3b4eac 
--- a/src/Cube/Cube.thy	Sun Sep 22 16:04:44 2024 +0200
+++ b/src/Cube/Cube.thy	Sun Sep 22 16:12:15 2024 +0200
@@ -29,8 +29,8 @@
 
 nonterminal context' and typing'
 syntax
-  "_Trueprop" :: "[context', typing'] \<Rightarrow> prop"  (\<open>(\<open>notation=\<open>infix Trueprop\<close>\<close>_/ \<turnstile> _)\<close>)
-  "_Trueprop1" :: "typing' \<Rightarrow> prop"  (\<open>(\<open>notation=\<open>prefix Trueprop\<close>\<close>_)\<close>)
+  "_Trueprop" :: "[context', typing'] \<Rightarrow> prop"  (\<open>(\<open>notation=judgment\<close>_/ \<turnstile> _)\<close>)
+  "_Trueprop1" :: "typing' \<Rightarrow> prop"  (\<open>(\<open>notation=judgment\<close>_)\<close>)
   "" :: "id \<Rightarrow> context'"  (\<open>_\<close>)
   "" :: "var \<Rightarrow> context'"  (\<open>_\<close>)
   "_MT_context" :: "context'"  (\<open>\<close>)
isabelle