equal
deleted
inserted
replaced
62 |
62 |
63 (* Enabledness conditions *) |
63 (* Enabledness conditions *) |
64 |
64 |
65 qed_goal "MemReturn_change" Memory.thy |
65 qed_goal "MemReturn_change" Memory.thy |
66 "MemReturn ch rs p .-> <MemReturn ch rs p>_<rtrner ch @ p, rs@p>" |
66 "MemReturn ch rs p .-> <MemReturn ch rs p>_<rtrner ch @ p, rs@p>" |
67 (fn _ => [ auto_tac (action_css addsimps2 [MemReturn_def,angle_def]) ]); |
67 (K [ force_tac (action_css addsimps2 [MemReturn_def,angle_def]) 1]); |
68 |
68 |
69 qed_goal "MemReturn_enabled" Memory.thy |
69 qed_goal "MemReturn_enabled" Memory.thy |
70 "!!p. base_var <rtrner ch @ p, rs@p> ==> \ |
70 "!!p. base_var <rtrner ch @ p, rs@p> ==> \ |
71 \ $(Calling ch p) .& ($(rs@p) .~= #NotAResult) \ |
71 \ $(Calling ch p) .& ($(rs@p) .~= #NotAResult) \ |
72 \ .-> $(Enabled (<MemReturn ch rs p>_<rtrner ch @ p, rs@p>))" |
72 \ .-> $(Enabled (<MemReturn ch rs p>_<rtrner ch @ p, rs@p>))" |