equal
deleted
inserted
replaced
32 fun map_ss f thy = Simpset.map (simpset_map (Proof_Context.init_global thy) f) thy; |
32 fun map_ss f thy = Simpset.map (simpset_map (Proof_Context.init_global thy) f) thy; |
33 |
33 |
34 fun simpset_default thy = the_default (Simpset.get thy); |
34 fun simpset_default thy = the_default (Simpset.get thy); |
35 |
35 |
36 |
36 |
37 (* diagonstic *) |
37 (* diagnostic *) |
38 |
38 |
39 val trace = Attrib.setup_config_bool @{binding "code_simp_trace"} (K false); |
39 val trace = Attrib.setup_config_bool @{binding "code_simp_trace"} (K false); |
40 |
40 |
41 fun set_trace ctxt = |
41 fun set_trace ctxt = |
42 let |
42 let |