--- a/src/HOL/IMP/Abs_Int1_parity.thy Sun Sep 16 10:33:25 2012 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy Sun Sep 16 11:50:03 2012 +0200
@@ -33,9 +33,9 @@
end
-text{* Instantiation of class @{class SL_top} with type @{typ parity}: *}
+text{* Instantiation of class @{class semilattice} with type @{typ parity}: *}
-instantiation parity :: SL_top
+instantiation parity :: semilattice
begin
definition join_parity where
@@ -118,11 +118,14 @@
subsubsection "Tests"
+(* FIXME dirty trick to get around some problem with the code generator *)
+lemma [code]: "L X = (L X :: 'av::semilattice st set)"
+by(rule refl)
+
definition "test1_parity =
''x'' ::= N 1;
WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 2)"
-
-value "show_acom_opt (AI_parity test1_parity)"
+value [code] "show_acom_opt (AI_parity test1_parity)"
definition "test2_parity =
''x'' ::= N 1;