equal
deleted
inserted
replaced
31 | _ => NONE; |
31 | _ => NONE; |
32 |
32 |
33 val tranformation_pairs = |
33 val tranformation_pairs = |
34 [("op -->", [mp]), ("op &", [conjunct1,conjunct2]), |
34 [("op -->", [mp]), ("op &", [conjunct1,conjunct2]), |
35 ("All", [spec]), ("True", []), ("False", []), |
35 ("All", [spec]), ("True", []), ("False", []), |
36 ("If", [if_bool_eq_conj RS iffD1])]; |
36 ("HOL.If", [if_bool_eq_conj RS iffD1])]; |
37 |
37 |
38 (* |
38 (* |
39 val mk_atomize: (string * thm list) list -> thm -> thm list |
39 val mk_atomize: (string * thm list) list -> thm -> thm list |
40 looks too specific to move it somewhere else |
40 looks too specific to move it somewhere else |
41 *) |
41 *) |