Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more specific markup for "judgment";
authorwenzelm
Sun, 22 Sep 2024 16:12:15 +0200
changeset 80923 6c9628a116cc
parent 80922 e0b958719301
child 80924 92d2ceda2370
more specific markup for "judgment";
src/Cube/Cube.thy file | annotate | diff | comparison | revisions
src/FOL/IFOL.thy file | annotate | diff | comparison | revisions
src/Pure/PIDE/markup_kind.ML file | annotate | diff | comparison | revisions
src/Sequents/ILL.thy file | annotate | diff | comparison | revisions
src/Sequents/LK0.thy file | annotate | diff | comparison | revisions 
--- 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>)
--- 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>
--- 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;
--- 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>)
 
--- 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>
isabelle