equal
deleted
inserted
replaced
66 by(auto simp: plus_const_cases split: const.split) |
66 by(auto simp: plus_const_cases split: const.split) |
67 qed |
67 qed |
68 |
68 |
69 permanent_interpretation Abs_Int |
69 permanent_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 defining AI_const = AI and step_const = step' and aval'_const = aval' |
72 .. |
72 .. |
73 |
73 |
74 |
74 |
75 subsubsection "Tests" |
75 subsubsection "Tests" |
76 |
76 |