equal
deleted
inserted
replaced
31 |
31 |
32 val imp_intr = impI |
32 val imp_intr = impI |
33 |
33 |
34 (*etac rev_cut_eq moves an equality to be the last premise. *) |
34 (*etac rev_cut_eq moves an equality to be the last premise. *) |
35 val rev_cut_eq = prove_goal IFOLP.thy |
35 val rev_cut_eq = prove_goal IFOLP.thy |
36 "[| p:a=b; !!x.x:a=b ==> f(x):R |] ==> ?p:R" |
36 "[| p:a=b; !!x. x:a=b ==> f(x):R |] ==> ?p:R" |
37 (fn prems => [ REPEAT(resolve_tac prems 1) ]); |
37 (fn prems => [ REPEAT(resolve_tac prems 1) ]); |
38 |
38 |
39 val rev_mp = rev_mp |
39 val rev_mp = rev_mp |
40 val subst = subst |
40 val subst = subst |
41 val sym = sym |
41 val sym = sym |