equal
deleted
inserted
replaced
52 = struct |
52 = struct |
53 |
53 |
54 |
54 |
55 (* beta contract the theorem *) |
55 (* beta contract the theorem *) |
56 fun beta_contract thm = |
56 fun beta_contract thm = |
57 equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm; |
57 Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm; |
58 |
58 |
59 (* beta-eta contract the theorem *) |
59 (* beta-eta contract the theorem *) |
60 fun beta_eta_contract thm = |
60 fun beta_eta_contract thm = |
61 let |
61 let |
62 val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm |
62 val thm2 = Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm |
63 val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2 |
63 val thm3 = Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2 |
64 in thm3 end; |
64 in thm3 end; |
65 |
65 |
66 |
66 |
67 (* to get the free names of a theorem (including hyps and flexes) *) |
67 (* to get the free names of a theorem (including hyps and flexes) *) |
68 fun usednames_of_thm th = |
68 fun usednames_of_thm th = |