equal
deleted
inserted
replaced
103 fun copy (ref ss) = ref ss: T; |
103 fun copy (ref ss) = ref ss: T; |
104 fun extend (ref ss) = ref (MetaSimplifier.inherit_context empty_ss ss); |
104 fun extend (ref ss) = ref (MetaSimplifier.inherit_context empty_ss ss); |
105 fun merge _ (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2)); |
105 fun merge _ (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2)); |
106 ); |
106 ); |
107 |
107 |
108 val _ = Context.>> GlobalSimpset.init; |
108 val _ = Context.>> (Context.map_theory GlobalSimpset.init); |
109 fun print_simpset thy = print_ss (! (GlobalSimpset.get thy)); |
109 fun print_simpset thy = print_ss (! (GlobalSimpset.get thy)); |
110 val get_simpset = ! o GlobalSimpset.get; |
110 val get_simpset = ! o GlobalSimpset.get; |
111 |
111 |
112 fun change_simpset_of thy f = CRITICAL (fn () => change (GlobalSimpset.get thy) f); |
112 fun change_simpset_of thy f = CRITICAL (fn () => change (GlobalSimpset.get thy) f); |
113 fun change_simpset f = CRITICAL (fn () => change_simpset_of (ML_Context.the_global_context ()) f); |
113 fun change_simpset f = CRITICAL (fn () => change_simpset_of (ML_Context.the_global_context ()) f); |
367 end; |
367 end; |
368 |
368 |
369 |
369 |
370 (* setup attributes *) |
370 (* setup attributes *) |
371 |
371 |
372 val _ = Context.>> |
372 val _ = Context.>> (Context.map_theory |
373 (Attrib.add_attributes |
373 (Attrib.add_attributes |
374 [(simpN, Attrib.add_del_args simp_add simp_del, "declaration of Simplifier rewrite rule"), |
374 [(simpN, Attrib.add_del_args simp_add simp_del, "declaration of Simplifier rewrite rule"), |
375 (congN, Attrib.add_del_args cong_add cong_del, "declaration of Simplifier congruence rule"), |
375 (congN, Attrib.add_del_args cong_add cong_del, "declaration of Simplifier congruence rule"), |
376 ("simproc", simproc_att, "declaration of simplification procedures"), |
376 ("simproc", simproc_att, "declaration of simplification procedures"), |
377 ("simplified", simplified, "simplified rule")]); |
377 ("simplified", simplified, "simplified rule")])); |
378 |
378 |
379 |
379 |
380 |
380 |
381 (** proof methods **) |
381 (** proof methods **) |
382 |
382 |