# HG changeset patch
# User nipkow
# Date 1365167605 -7200
# Node ID c839ccebf2fbf22aedf33b04ae6d3f9bd9cdf000
# Parent  1194b438426a7fc85691a30596415d777838b5e9
tuned

diff -r 1194b438426a -r c839ccebf2fb src/HOL/IMP/Abs_Int1_parity.thy
--- a/src/HOL/IMP/Abs_Int1_parity.thy	Thu Apr 04 22:46:14 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy	Fri Apr 05 15:13:25 2013 +0200
@@ -53,7 +53,7 @@
 begin
 
 definition sup_parity where
-"x \<squnion> y = (if x \<le> y then y else if y \<le> x then x else Either)"
+"x \<squnion> y = (if x = y then x else Either)"
 
 definition top_parity where
 "\<top> = Either"