equal
deleted
inserted
replaced
43 |
43 |
44 fun rulify_elim_conv ct = |
44 fun rulify_elim_conv ct = |
45 if is_atomic (Logic.strip_imp_concl (term_of ct)) then Conv.all_conv ct |
45 if is_atomic (Logic.strip_imp_concl (term_of ct)) then Conv.all_conv ct |
46 else Conv.concl_conv (length (Logic.strip_imp_prems (term_of ct))) |
46 else Conv.concl_conv (length (Logic.strip_imp_prems (term_of ct))) |
47 (Conv.rewr_conv (Thm.symmetric Data.atomize_elimL) then_conv |
47 (Conv.rewr_conv (Thm.symmetric Data.atomize_elimL) then_conv |
48 MetaSimplifier.rewrite true (map Thm.symmetric |
48 Raw_Simplifier.rewrite true (map Thm.symmetric |
49 [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct |
49 [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct |
50 |
50 |
51 fun rulify_elim th = Simplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th); |
51 fun rulify_elim th = Simplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th); |
52 |
52 |
53 (* Decompose elimination rule of the form |
53 (* Decompose elimination rule of the form |