--- a/src/Sequents/ILL.thy Mon Jan 11 21:16:38 2016 +0100
+++ b/src/Sequents/ILL.thy Mon Jan 11 21:20:44 2016 +0100
@@ -12,14 +12,12 @@
tens :: "[o, o] \<Rightarrow> o" (infixr "><" 35)
limp :: "[o, o] \<Rightarrow> o" (infixr "-o" 45)
- liff :: "[o, o] \<Rightarrow> o" (infixr "o-o" 45)
FShriek :: "o \<Rightarrow> o" ("! _" [100] 1000)
lconj :: "[o, o] \<Rightarrow> o" (infixr "&&" 35)
ldisj :: "[o, o] \<Rightarrow> o" (infixr "++" 35)
zero :: "o" ("0")
top :: "o" ("1")
eye :: "o" ("I")
- aneg :: "o\<Rightarrow>o" ("~_")
(* context manipulation *)
@@ -47,11 +45,11 @@
(@{const_syntax PromAux}, K (three_seq_tr' @{syntax_const "_PromAux"}))]
\<close>
-defs
+definition liff :: "[o, o] \<Rightarrow> o" (infixr "o-o" 45)
+ where "P o-o Q == (P -o Q) >< (Q -o P)"
-liff_def: "P o-o Q == (P -o Q) >< (Q -o P)"
-
-aneg_def: "~A == A -o 0"
+definition aneg :: "o\<Rightarrow>o" ("~_")
+ where "~A == A -o 0"
axiomatization where
--- a/src/Sequents/Modal0.thy Mon Jan 11 21:16:38 2016 +0100
+++ b/src/Sequents/Modal0.thy Mon Jan 11 21:20:44 2016 +0100
@@ -12,8 +12,6 @@
consts
box :: "o\<Rightarrow>o" ("[]_" [50] 50)
dia :: "o\<Rightarrow>o" ("<>_" [50] 50)
- strimp :: "[o,o]\<Rightarrow>o" (infixr "--<" 25)
- streqv :: "[o,o]\<Rightarrow>o" (infixr ">-<" 25)
Lstar :: "two_seqi"
Rstar :: "two_seqi"
@@ -36,9 +34,11 @@
(@{const_syntax Rstar}, K (star_tr' @{syntax_const "_Rstar"}))]
\<close>
-defs
- strimp_def: "P --< Q == [](P \<longrightarrow> Q)"
- streqv_def: "P >-< Q == (P --< Q) \<and> (Q --< P)"
+definition strimp :: "[o,o]\<Rightarrow>o" (infixr "--<" 25)
+ where "P --< Q == [](P \<longrightarrow> Q)"
+
+definition streqv :: "[o,o]\<Rightarrow>o" (infixr ">-<" 25)
+ where "P >-< Q == (P --< Q) \<and> (Q --< P)"
lemmas rewrite_rls = strimp_def streqv_def