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_goalw_cterm [] (cterm_of (sign_of (theory_of_thm iffD)) |
22 val lift = |
23 (read "[| !!x::'b::logic. Q(x) == R(x) |] ==> \ |
23 let val ct = read_cterm (#sign(rep_thm iffD)) |
24 \P(%x.Q(x)) == P(%x.R(x))::'a::logic")) |
24 ("[| !!x::'b::logic. Q(x) == R(x) |] ==> \ |
25 (fn [prem] => [rewtac prem, rtac reflexive_thm 1]); |
25 \P(%x.Q(x)) == P(%x.R(x))::'a::logic",propT) |
|
26 in prove_goalw_cterm [] ct |
|
27 (fn [prem] => [rewtac prem, rtac reflexive_thm 1]) |
|
28 end; |
26 |
29 |
27 val trlift = lift RS transitive_thm; |
30 val trlift = lift RS transitive_thm; |
28 val _ $ (Var(P,PT)$_) $ _ = concl_of trlift; |
31 val _ $ (Var(P,PT)$_) $ _ = concl_of trlift; |
29 |
32 |
30 fun contains cmap = |
33 fun contains cmap = |