57 val deleqcongs: simpset * thm list -> simpset |
57 val deleqcongs: simpset * thm list -> simpset |
58 val addcongs: simpset * thm list -> simpset |
58 val addcongs: simpset * thm list -> simpset |
59 val delcongs: simpset * thm list -> simpset |
59 val delcongs: simpset * thm list -> simpset |
60 val addsimprocs: simpset * simproc list -> simpset |
60 val addsimprocs: simpset * simproc list -> simpset |
61 val delsimprocs: simpset * simproc list -> simpset |
61 val delsimprocs: simpset * simproc list -> simpset |
|
62 val mksimps: simpset -> thm -> thm list |
62 val setmksimps: simpset * (thm -> thm list) -> simpset |
63 val setmksimps: simpset * (thm -> thm list) -> simpset |
63 val setmkcong: simpset * (thm -> thm) -> simpset |
64 val setmkcong: simpset * (thm -> thm) -> simpset |
64 val setmksym: simpset * (thm -> thm option) -> simpset |
65 val setmksym: simpset * (thm -> thm option) -> simpset |
65 val setmkeqTrue: simpset * (thm -> thm option) -> simpset |
66 val setmkeqTrue: simpset * (thm -> thm option) -> simpset |
66 val settermless: simpset * (term * term -> bool) -> simpset |
67 val settermless: simpset * (term * term -> bool) -> simpset |
545 comb_simps del_rrule (map mk_rrule2 o mk_rrule ss) (ss, thms); |
546 comb_simps del_rrule (map mk_rrule2 o mk_rrule ss) (ss, thms); |
546 |
547 |
547 fun add_simp thm ss = ss addsimps [thm]; |
548 fun add_simp thm ss = ss addsimps [thm]; |
548 fun del_simp thm ss = ss delsimps [thm]; |
549 fun del_simp thm ss = ss delsimps [thm]; |
549 |
550 |
|
551 |
550 (* congs *) |
552 (* congs *) |
551 |
553 |
552 fun cong_name (Const (a, _)) = SOME a |
554 fun cong_name (Const (a, _)) = SOME a |
553 | cong_name (Free (a, _)) = SOME ("Free: " ^ a) |
555 | cong_name (Free (a, _)) = SOME ("Free: " ^ a) |
554 | cong_name _ = NONE; |
556 | cong_name _ = NONE; |
691 val mk_rews' = {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True', |
693 val mk_rews' = {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True', |
692 reorient = reorient'}; |
694 reorient = reorient'}; |
693 in (congs, procs, mk_rews', termless, subgoal_tac, loop_tacs, solvers) end); |
695 in (congs, procs, mk_rews', termless, subgoal_tac, loop_tacs, solvers) end); |
694 |
696 |
695 in |
697 in |
|
698 |
|
699 val mksimps = #mk o #mk_rews o #2 o rep_ss; |
696 |
700 |
697 fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) => |
701 fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) => |
698 (mk, mk_cong, mk_sym, mk_eq_True, reorient)); |
702 (mk, mk_cong, mk_sym, mk_eq_True, reorient)); |
699 |
703 |
700 fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, _, mk_sym, mk_eq_True, reorient) => |
704 fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, _, mk_sym, mk_eq_True, reorient) => |