| changeset 51826 | 054a40461449 |
| parent 51711 | df3426139651 |
| child 52046 | bc01725d7918 |
--- a/src/HOL/IMP/Abs_Int1_parity.thy Mon Apr 29 18:52:35 2013 +0200 +++ b/src/HOL/IMP/Abs_Int1_parity.thy Tue Apr 30 03:18:07 2013 +0200 @@ -47,9 +47,9 @@ end -text{* Instantiation of class @{class semilattice} with type @{typ parity}: *} +text{* Instantiation of class @{class semilattice_sup_top} with type @{typ parity}: *} -instantiation parity :: semilattice +instantiation parity :: semilattice_sup_top begin definition sup_parity where