# HG changeset patch
# User wenzelm
# Date 1452543644 -3600
# Node ID bdab93ccfaf83d50a6b81f58ef264d996c5b175d
# Parent  3c9a0985e6be9f08e2c997ef3694bb6b9a26ecca
eliminated old defs;

diff -r 3c9a0985e6be -r bdab93ccfaf8 src/Sequents/ILL.thy
--- 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
diff -r 3c9a0985e6be -r bdab93ccfaf8 src/Sequents/Modal0.thy
--- 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