| 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