equal
deleted
inserted
replaced
89 apply (rule hoare_derivs.Ass [THEN conseq1]) |
89 apply (rule hoare_derivs.Ass [THEN conseq1]) |
90 apply (clarsimp simp: Arg_Res_simps) |
90 apply (clarsimp simp: Arg_Res_simps) |
91 apply (rule hoare_derivs.Comp) |
91 apply (rule hoare_derivs.Comp) |
92 apply (rule_tac [2] hoare_derivs.Ass) |
92 apply (rule_tac [2] hoare_derivs.Ass) |
93 apply clarsimp |
93 apply clarsimp |
94 apply (rule_tac Q = "%Z s. ?P Z s & Res_ok Z s" in hoare_derivs.Comp) |
94 apply (rule_tac Q = "%Z s. P Z s & Res_ok Z s" and P = P for P in hoare_derivs.Comp) |
95 apply (rule export_s) |
95 apply (rule export_s) |
96 apply (rule_tac I1 = "%Z l. Z = l Arg & 0 < Z" and Q1 = "Res_ok" in Call_invariant [THEN conseq12]) |
96 apply (rule_tac I1 = "%Z l. Z = l Arg & 0 < Z" and Q1 = "Res_ok" in Call_invariant [THEN conseq12]) |
97 apply (rule single_asm [THEN conseq2]) |
97 apply (rule single_asm [THEN conseq2]) |
98 apply (clarsimp simp: Arg_Res_simps) |
98 apply (clarsimp simp: Arg_Res_simps) |
99 apply (force simp: Arg_Res_simps) |
99 apply (force simp: Arg_Res_simps) |