equal
deleted
inserted
replaced
30 *************************************************************) |
30 *************************************************************) |
31 |
31 |
32 val lift = |
32 val lift = |
33 let val ct = read_cterm (#sign(rep_thm iffD)) |
33 let val ct = read_cterm (#sign(rep_thm iffD)) |
34 ("[| !!x::'b::logic. Q(x) == R(x) |] ==> \ |
34 ("[| !!x::'b::logic. Q(x) == R(x) |] ==> \ |
35 \P(%x.Q(x)) == P(%x.R(x))::'a::logic",propT) |
35 \P(%x. Q(x)) == P(%x. R(x))::'a::logic",propT) |
36 in prove_goalw_cterm [] ct |
36 in prove_goalw_cterm [] ct |
37 (fn [prem] => [rewtac prem, rtac reflexive_thm 1]) |
37 (fn [prem] => [rewtac prem, rtac reflexive_thm 1]) |
38 end; |
38 end; |
39 |
39 |
40 val trlift = lift RS transitive_thm; |
40 val trlift = lift RS transitive_thm; |