--- a/src/HOL/IMP/Abs_Int1_const.thy Sun Sep 16 10:33:25 2012 +0200
+++ b/src/HOL/IMP/Abs_Int1_const.thy Sun Sep 16 11:50:03 2012 +0200
@@ -20,7 +20,7 @@
(case (a1,a2) of (Const m, Const n) \<Rightarrow> Const(m+n) | _ \<Rightarrow> Any)"
by(auto split: prod.split const.split)
-instantiation const :: SL_top
+instantiation const :: semilattice
begin
fun le_const where
@@ -74,6 +74,10 @@
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 "steps c i = (step_const(top c) ^^ i) (bot c)"
value "show_acom (steps test1_const 0)"