# HG changeset patch
# User wenzelm
# Date 1727014335 -7200
# Node ID 6c9628a116ccaec568cfe289743a5d093a3f0d4e
# Parent  e0b958719301e3b48bb4f4376ca64220a5de29cf
more specific markup for "judgment";

diff -r e0b958719301 -r 6c9628a116cc src/Cube/Cube.thy
--- 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>)
diff -r e0b958719301 -r 6c9628a116cc src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Sun Sep 22 16:04:44 2024 +0200
+++ b/src/FOL/IFOL.thy	Sun Sep 22 16:12:15 2024 +0200
@@ -32,7 +32,7 @@
 typedecl o
 
 judgment
-  Trueprop :: \<open>o \<Rightarrow> prop\<close>  (\<open>(_)\<close> 5)
+  Trueprop :: \<open>o \<Rightarrow> prop\<close>  (\<open>(\<open>notation=judgment\<close>_)\<close> 5)
 
 
 subsubsection \<open>Equality\<close>
diff -r e0b958719301 -r 6c9628a116cc src/Pure/PIDE/markup_kind.ML
--- a/src/Pure/PIDE/markup_kind.ML	Sun Sep 22 16:04:44 2024 +0200
+++ b/src/Pure/PIDE/markup_kind.ML	Sun Sep 22 16:12:15 2024 +0200
@@ -24,6 +24,7 @@
   val markup_type_application: Markup.T
   val markup_application: Markup.T
   val markup_abstraction: Markup.T
+  val markup_judgment: Markup.T
 end;
 
 structure Markup_Kind: MARKUP_KIND =
@@ -101,4 +102,6 @@
 val markup_application = setup_notation (Binding.make ("application", \<^here>));
 val markup_abstraction = setup_notation (Binding.make ("abstraction", \<^here>));
 
+val markup_judgment = setup_notation (Binding.make ("judgment", \<^here>));
+
 end;
diff -r e0b958719301 -r 6c9628a116cc src/Sequents/ILL.thy
--- a/src/Sequents/ILL.thy	Sun Sep 22 16:04:44 2024 +0200
+++ b/src/Sequents/ILL.thy	Sun Sep 22 16:12:15 2024 +0200
@@ -29,7 +29,7 @@
   PromAux :: "three_seqi"
 
 syntax
-  "_Trueprop" :: "single_seqe" (\<open>(\<open>notation=\<open>infix Trueprop\<close>\<close>(_)/ \<turnstile> (_))\<close> [6,6] 5)
+  "_Trueprop" :: "single_seqe" (\<open>(\<open>notation=judgment\<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>)
 
diff -r e0b958719301 -r 6c9628a116cc src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Sun Sep 22 16:04:44 2024 +0200
+++ b/src/Sequents/LK0.thy	Sun Sep 22 16:12:15 2024 +0200
@@ -34,7 +34,7 @@
   Ex           :: "('a \<Rightarrow> o) \<Rightarrow> o"   (binder \<open>\<exists>\<close> 10)
 
 syntax
- "_Trueprop"    :: "two_seqe" (\<open>(\<open>notation=\<open>infix Trueprop\<close>\<close>(_)/ \<turnstile> (_))\<close> [6,6] 5)
+ "_Trueprop"    :: "two_seqe" (\<open>(\<open>notation=judgment\<close>(_)/ \<turnstile> (_))\<close> [6,6] 5)
 
 parse_translation \<open>[(\<^syntax_const>\<open>_Trueprop\<close>, K (two_seq_tr \<^const_syntax>\<open>Trueprop\<close>))]\<close>
 print_translation \<open>[(\<^const_syntax>\<open>Trueprop\<close>, K (two_seq_tr' \<^syntax_const>\<open>_Trueprop\<close>))]\<close>