equal
deleted
inserted
replaced
17 *) |
17 *) |
18 |
18 |
19 fun mk_case_split_tac iffD = |
19 fun mk_case_split_tac iffD = |
20 let |
20 let |
21 |
21 |
22 val lift = prove_goal Pure.thy |
22 val lift = prove_goalw_cterm [] (cterm_of (sign_of (theory_of_thm iffD)) |
23 "[| !!x::'b::logic. Q(x) == R(x) |] ==> P(%x.Q(x)) == P(%x.R(x))::'a::logic" |
23 (read "[| !!x::'b::logic. Q(x) == R(x) |] ==> \ |
24 (fn [prem] => [rewtac prem, rtac reflexive_thm 1]); |
24 \P(%x.Q(x)) == P(%x.R(x))::'a::logic")) |
|
25 (fn [prem] => [rewtac prem, rtac reflexive_thm 1]); |
25 |
26 |
26 val trlift = lift RS transitive_thm; |
27 val trlift = lift RS transitive_thm; |
27 val _ $ (Var(P,PT)$_) $ _ = concl_of trlift; |
28 val _ $ (Var(P,PT)$_) $ _ = concl_of trlift; |
28 |
29 |
29 fun contains cmap = |
30 fun contains cmap = |