equal
deleted
inserted
replaced
367 |
367 |
368 |
368 |
369 (* rulify setup *) |
369 (* rulify setup *) |
370 |
370 |
371 local |
371 local |
372 val ss = FOL_basic_ss addsimps (Drule.norm_hhf_eq :: map Thm.symmetric (thms "atomize")); |
372 val ss = FOL_basic_ss addsimps |
|
373 [Drule.norm_hhf_eq, Thm.symmetric (thm "atomize_all"), Thm.symmetric (thm "atomize_imp")]; |
373 in |
374 in |
374 |
375 |
375 structure Rulify = RulifyFun |
376 structure Rulify = RulifyFun |
376 (val make_meta = Simplifier.simplify ss |
377 (val make_meta = Simplifier.simplify ss |
377 val full_make_meta = Simplifier.full_simplify ss); |
378 val full_make_meta = Simplifier.full_simplify ss); |