equal
deleted
inserted
replaced
112 instantiated abstract interpreter which we call AI: *} |
112 instantiated abstract interpreter which we call AI: *} |
113 |
113 |
114 interpretation Abs_Int |
114 interpretation Abs_Int |
115 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity |
115 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity |
116 defines aval_parity is aval' and step_parity is step' and AI_parity is AI |
116 defines aval_parity is aval' and step_parity is step' and AI_parity is AI |
117 proof qed |
117 .. |
118 |
118 |
119 |
119 |
120 subsubsection "Tests" |
120 subsubsection "Tests" |
121 |
121 |
122 definition "test1_parity = |
122 definition "test1_parity = |