equal
deleted
inserted
replaced
59 next |
59 next |
60 case goal2 thus ?case |
60 case goal2 thus ?case |
61 by(cases a1, cases a2, simp, simp, cases a2, simp, simp) |
61 by(cases a1, cases a2, simp, simp, cases a2, simp, simp) |
62 qed |
62 qed |
63 |
63 |
64 interpretation Abs_Int rep_cval Const plus_cval "(iter_above 3)" |
64 interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)" |
65 defines AI_const is AI |
65 defines AI_const is AI |
66 and aval'_const is aval' |
66 and aval'_const is aval' |
67 proof qed (auto simp: iter_above_pfp) |
67 proof qed (auto simp: iter'_pfp_above) |
68 |
68 |
69 text{* Straight line code: *} |
69 text{* Straight line code: *} |
70 definition "test1_const = |
70 definition "test1_const = |
71 ''y'' ::= N 7; |
71 ''y'' ::= N 7; |
72 ''z'' ::= Plus (V ''y'') (N 2); |
72 ''z'' ::= Plus (V ''y'') (N 2); |