equal
deleted
inserted
replaced
30 ); |
30 ); |
31 |
31 |
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 ctxt some_ss = the_default (Simpset.get (Proof_Context.theory_of ctxt)) some_ss; |
34 fun simpset_default ctxt some_ss = the_default (Simpset.get (Proof_Context.theory_of ctxt)) some_ss; |
35 |
|
36 (*fun simp_ctxt_default ctxt some_ss = |
|
37 Proof_Context.init_global ctxt |
|
38 |> put_simpset (simpset_default ctxt some_ss);*) |
|
39 |
35 |
40 |
36 |
41 (* diagnostic *) |
37 (* diagnostic *) |
42 |
38 |
43 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); |