src/HOL/IMP/Abs_Int1_parity.thy
changeset 52504 52cd8bebc3b6
parent 52046 bc01725d7918
child 52525 1e09c034d6c3
--- a/src/HOL/IMP/Abs_Int1_parity.thy	Tue Jul 02 20:47:32 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy	Wed Jul 03 16:07:00 2013 +0200
@@ -102,7 +102,7 @@
 text{* First we instantiate the abstract value interface and prove that the
 functions on type @{typ parity} have all the necessary properties: *}
 
-interpretation Val_abs
+interpretation Val_semilattice
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
 proof txt{* of the locale axioms *}
   fix a b :: parity