equal
deleted
inserted
replaced
88 (rtac theleast2 1), |
88 (rtac theleast2 1), |
89 (etac hoare_lemma7 1) |
89 (etac hoare_lemma7 1) |
90 ]); |
90 ]); |
91 |
91 |
92 val hoare_lemma28 = prove_goal HOLCF.thy |
92 val hoare_lemma28 = prove_goal HOLCF.thy |
93 "b1[y::'a]=UU::tr ==> b1[UU] = UU" |
93 "b1[y::'a]=(UU::tr) ==> b1[UU] = UU" |
94 (fn prems => |
94 (fn prems => |
95 [ |
95 [ |
96 (cut_facts_tac prems 1), |
96 (cut_facts_tac prems 1), |
97 (etac (flat_tr RS flat_codom RS disjE) 1), |
97 (etac (flat_tr RS flat_codom RS disjE) 1), |
98 (atac 1), |
98 (atac 1), |