equal
deleted
inserted
replaced
31 structure BNF_FP_Def_Sugar_Tactics : BNF_FP_DEF_SUGAR_TACTICS = |
31 structure BNF_FP_Def_Sugar_Tactics : BNF_FP_DEF_SUGAR_TACTICS = |
32 struct |
32 struct |
33 |
33 |
34 open BNF_Tactics |
34 open BNF_Tactics |
35 open BNF_Util |
35 open BNF_Util |
36 open BNF_FP |
36 open BNF_FP_Util |
37 |
37 |
38 val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)}; |
38 val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)}; |
39 val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)}; |
39 val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)}; |
40 |
40 |
41 val sum_prod_thms_map = @{thms id_apply map_pair_simp prod.cases sum.cases sum_map.simps}; |
41 val sum_prod_thms_map = @{thms id_apply map_pair_simp prod.cases sum.cases sum_map.simps}; |