# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1576973744 -32400
# Node ID 222dd3869ab06f9abf17b2663840fd702ad5a858
# Parent  bfe7d83cf9ba9908c99f7ab74730fd0e3b7351ef
remove wrong ==>

diff -r bfe7d83cf9ba -r 222dd3869ab0 HoareSoundness.agda
--- a/HoareSoundness.agda	Sat Dec 21 21:12:07 2019 +0900
+++ b/HoareSoundness.agda	Sun Dec 22 09:15:44 2019 +0900
@@ -45,9 +45,6 @@
 _\/_ : Cond -> Cond -> Cond
 b1 \/ b2 = neg (neg b1 /\ neg b2)
 
-_==>_ : Cond -> Cond -> Cond
-b1 ==> b2 = neg (b1 \/ b2)
-
 when : {X  Y  Z : Set} -> (X -> Z) -> (Y -> Z) ->
        X ⊎ Y -> Z
 when f g (inj₁ x) = f x
diff -r bfe7d83cf9ba -r 222dd3869ab0 whileTestPrimProof.agda
--- a/whileTestPrimProof.agda	Sat Dec 21 21:12:07 2019 +0900
+++ b/whileTestPrimProof.agda	Sun Dec 22 09:15:44 2019 +0900
@@ -207,9 +207,6 @@
 _\/_ : Cond -> Cond -> Cond
 b1 \/ b2 = neg (neg b1 /\ neg b2)
 
-_==>_ : Cond -> Cond -> Cond
-b1 ==> b2 = neg (b1 \/ b2)
-
 SemCond : Cond -> State -> Set
 SemCond c p = c p ≡ true