eliminated old defs;
authorwenzelm
Mon Jan 11 21:20:44 2016 +0100 (2016-01-11)
changeset 62144bdab93ccfaf8
parent 62143 3c9a0985e6be
child 62145 5b946c81dfbf
eliminated old defs;
src/Sequents/ILL.thy
src/Sequents/Modal0.thy
     1.1 --- a/src/Sequents/ILL.thy	Mon Jan 11 21:16:38 2016 +0100
     1.2 +++ b/src/Sequents/ILL.thy	Mon Jan 11 21:20:44 2016 +0100
     1.3 @@ -12,14 +12,12 @@
     1.4  
     1.5    tens :: "[o, o] \<Rightarrow> o"        (infixr "><" 35)
     1.6    limp :: "[o, o] \<Rightarrow> o"        (infixr "-o" 45)
     1.7 -  liff :: "[o, o] \<Rightarrow> o"        (infixr "o-o" 45)
     1.8    FShriek :: "o \<Rightarrow> o"          ("! _" [100] 1000)
     1.9    lconj :: "[o, o] \<Rightarrow> o"       (infixr "&&" 35)
    1.10    ldisj :: "[o, o] \<Rightarrow> o"       (infixr "++" 35)
    1.11    zero :: "o"                  ("0")
    1.12    top :: "o"                   ("1")
    1.13    eye :: "o"                   ("I")
    1.14 -  aneg :: "o\<Rightarrow>o"               ("~_")
    1.15  
    1.16  
    1.17    (* context manipulation *)
    1.18 @@ -47,11 +45,11 @@
    1.19     (@{const_syntax PromAux}, K (three_seq_tr' @{syntax_const "_PromAux"}))]
    1.20  \<close>
    1.21  
    1.22 -defs
    1.23 +definition liff :: "[o, o] \<Rightarrow> o"  (infixr "o-o" 45)
    1.24 +  where "P o-o Q == (P -o Q) >< (Q -o P)"
    1.25  
    1.26 -liff_def:        "P o-o Q == (P -o Q) >< (Q -o P)"
    1.27 -
    1.28 -aneg_def:        "~A == A -o 0"
    1.29 +definition aneg :: "o\<Rightarrow>o"  ("~_")
    1.30 +  where "~A == A -o 0"
    1.31  
    1.32  
    1.33  axiomatization where
     2.1 --- a/src/Sequents/Modal0.thy	Mon Jan 11 21:16:38 2016 +0100
     2.2 +++ b/src/Sequents/Modal0.thy	Mon Jan 11 21:20:44 2016 +0100
     2.3 @@ -12,8 +12,6 @@
     2.4  consts
     2.5    box           :: "o\<Rightarrow>o"       ("[]_" [50] 50)
     2.6    dia           :: "o\<Rightarrow>o"       ("<>_" [50] 50)
     2.7 -  strimp        :: "[o,o]\<Rightarrow>o"   (infixr "--<" 25)
     2.8 -  streqv        :: "[o,o]\<Rightarrow>o"   (infixr ">-<" 25)
     2.9    Lstar         :: "two_seqi"
    2.10    Rstar         :: "two_seqi"
    2.11  
    2.12 @@ -36,9 +34,11 @@
    2.13    (@{const_syntax Rstar}, K (star_tr' @{syntax_const "_Rstar"}))]
    2.14  \<close>
    2.15  
    2.16 -defs
    2.17 -  strimp_def:    "P --< Q == [](P \<longrightarrow> Q)"
    2.18 -  streqv_def:    "P >-< Q == (P --< Q) \<and> (Q --< P)"
    2.19 +definition strimp :: "[o,o]\<Rightarrow>o"   (infixr "--<" 25)
    2.20 +  where "P --< Q == [](P \<longrightarrow> Q)"
    2.21 +
    2.22 +definition streqv :: "[o,o]\<Rightarrow>o"   (infixr ">-<" 25)
    2.23 +  where "P >-< Q == (P --< Q) \<and> (Q --< P)"
    2.24  
    2.25  
    2.26  lemmas rewrite_rls = strimp_def streqv_def