# HG changeset patch
# User wenzelm
# Date 1729449173 -7200
# Node ID d1170873976e045bd24b90d386878439ac79d099
# Parent  b5836dd39018fadbf485704060370dfb1c898a13
clarified concrete vs. abstract syntax;

diff -r b5836dd39018 -r d1170873976e src/Sequents/ILL_predlog.thy
--- a/src/Sequents/ILL_predlog.thy	Sun Oct 20 18:47:42 2024 +0200
+++ b/src/Sequents/ILL_predlog.thy	Sun Oct 20 20:32:53 2024 +0200
@@ -3,19 +3,16 @@
 begin
 
 typedecl plf
-
-consts
-  conj :: "[plf,plf] \<Rightarrow> plf"   (infixr \<open>&\<close> 35)
-  disj :: "[plf,plf] \<Rightarrow> plf"   (infixr \<open>|\<close> 35)
-  impl :: "[plf,plf] \<Rightarrow> plf"   (infixr \<open>>\<close> 35)
-  eq :: "[plf,plf] \<Rightarrow> plf"   (infixr \<open>=\<close> 35)
-  ff :: "plf"    (\<open>ff\<close>)
-
-  PL    :: "plf \<Rightarrow> o"      (\<open>[* / _ / *]\<close> [] 100)
+consts "PL" :: "plf \<Rightarrow> o"
 
 syntax
+  "_PL" :: "plf \<Rightarrow> o"      (\<open>[* / _ / *]\<close> [] 100)
+  "_conj" :: "[plf,plf] \<Rightarrow> plf"   (infixr \<open>&\<close> 35)
+  "_disj" :: "[plf,plf] \<Rightarrow> plf"   (infixr \<open>|\<close> 35)
+  "_impl" :: "[plf,plf] \<Rightarrow> plf"   (infixr \<open>>\<close> 35)
+  "_eq" :: "[plf,plf] \<Rightarrow> plf"   (infixr \<open>=\<close> 35)
+  "_ff" :: "plf"    (\<open>ff\<close>)
   "_NG" :: "plf \<Rightarrow> plf"   (\<open>- _ \<close> [50] 55)
-
 translations
   "[* A & B *]" \<rightleftharpoons> "[*A*] && [*B*]"
   "[* A | B *]" \<rightleftharpoons> "![*A*] ++ ![*B*]"
@@ -24,6 +21,7 @@
   "[* A = B *]" \<rightharpoonup> "[* (A > B) & (B > A) *]"
 
   "[* A > B *]" \<rightleftharpoons> "![*A*] -o [*B*]"
+  "_PL" \<rightleftharpoons> "CONST PL"
 
 (* another translations for linear implication:
   "[* A > B *]" == "!([*A*] -o [*B*])" *)