equal
deleted
inserted
replaced
74 *************************************************************) |
74 *************************************************************) |
75 |
75 |
76 val meta_iffD = Data.meta_eq_to_iff RS Data.iffD; |
76 val meta_iffD = Data.meta_eq_to_iff RS Data.iffD; |
77 val lift = |
77 val lift = |
78 let val ct = read_cterm (#sign(rep_thm Data.iffD)) |
78 let val ct = read_cterm (#sign(rep_thm Data.iffD)) |
79 ("[| !!x. (Q::('b::logic)=>('c::logic))(x) == R(x) |] ==> \ |
79 ("[| !!x. (Q::('b::{})=>('c::{}))(x) == R(x) |] ==> \ |
80 \P(%x. Q(x)) == P(%x. R(x))::'a::logic",propT) |
80 \P(%x. Q(x)) == P(%x. R(x))::'a::{}",propT) |
81 in prove_goalw_cterm [] ct |
81 in prove_goalw_cterm [] ct |
82 (fn [prem] => [rewtac prem, rtac reflexive_thm 1]) |
82 (fn [prem] => [rewtac prem, rtac reflexive_thm 1]) |
83 end; |
83 end; |
84 |
84 |
85 val trlift = lift RS transitive_thm; |
85 val trlift = lift RS transitive_thm; |