equal
deleted
inserted
replaced
67 qed |
67 qed |
68 |
68 |
69 interpretation Abs_Int |
69 interpretation Abs_Int |
70 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
70 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const |
71 defines AI_const is AI and step_const is step' and aval'_const is aval' |
71 defines AI_const is AI and step_const is step' and aval'_const is aval' |
72 proof qed |
72 .. |
73 |
73 |
74 |
74 |
75 subsubsection "Tests" |
75 subsubsection "Tests" |
76 |
76 |
77 value "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test1_const))" |
77 value "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test1_const))" |