equal
deleted
inserted
replaced
19 |
19 |
20 open Nominal_Permeq; |
20 open Nominal_Permeq; |
21 open Nominal_ThmDecls; |
21 open Nominal_ThmDecls; |
22 |
22 |
23 val atomize_conv = |
23 val atomize_conv = |
24 MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE)) |
24 Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE)) |
25 (HOL_basic_ss addsimps @{thms induct_atomize}); |
25 (HOL_basic_ss addsimps @{thms induct_atomize}); |
26 val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv); |
26 val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv); |
27 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 |
27 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 |
28 (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt)); |
28 (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt)); |
29 |
29 |