equal
deleted
inserted
replaced
13 |
13 |
14 signature BASIC_SIMPLIFIER = |
14 signature BASIC_SIMPLIFIER = |
15 sig |
15 sig |
16 type simproc |
16 type simproc |
17 val mk_simproc: string -> cterm list |
17 val mk_simproc: string -> cterm list |
|
18 -> (Sign.sg -> thm list -> term -> thm option) -> simproc |
|
19 val simproc: Sign.sg -> string -> string list |
|
20 -> (Sign.sg -> thm list -> term -> thm option) -> simproc |
|
21 val simproc_i: Sign.sg -> string -> term list |
18 -> (Sign.sg -> thm list -> term -> thm option) -> simproc |
22 -> (Sign.sg -> thm list -> term -> thm option) -> simproc |
19 type solver |
23 type solver |
20 val mk_solver: string -> (thm list -> int -> tactic) -> solver |
24 val mk_solver: string -> (thm list -> int -> tactic) -> solver |
21 type simpset |
25 type simpset |
22 val empty_ss: simpset |
26 val empty_ss: simpset |
124 Simproc of string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp; |
128 Simproc of string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp; |
125 |
129 |
126 fun mk_simproc name lhss proc = |
130 fun mk_simproc name lhss proc = |
127 Simproc (name, map (Thm.cterm_fun Logic.varify) lhss, proc, stamp ()); |
131 Simproc (name, map (Thm.cterm_fun Logic.varify) lhss, proc, stamp ()); |
128 |
132 |
|
133 fun simproc sg name ss = |
|
134 mk_simproc name (map (fn s => Thm.read_cterm sg (s, TypeInfer.logicT)) ss); |
|
135 fun simproc_i sg name = mk_simproc name o map (Thm.cterm_of sg); |
|
136 |
129 fun rep_simproc (Simproc args) = args; |
137 fun rep_simproc (Simproc args) = args; |
130 |
138 |
131 |
139 |
132 |
140 |
133 (** solvers **) |
141 (** solvers **) |