src/Sequents/Modal0.thy
changeset 62144 bdab93ccfaf8
parent 61386 0a29a984a91b
child 69605 3dda49e08b9d
--- 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