equal
deleted
inserted
replaced
171 end; |
171 end; |
172 |
172 |
173 |
173 |
174 (* basic combinations *) |
174 (* basic combinations *) |
175 |
175 |
176 fun fast_simp_tac ctxt i = |
|
177 let val _ = legacy_feature "Old name 'fastsimp' - use 'fastforce' instead" |
|
178 in Classical.fast_tac (addss ctxt) i end; |
|
179 |
|
180 val fast_force_tac = Classical.fast_tac o addss; |
176 val fast_force_tac = Classical.fast_tac o addss; |
181 val slow_simp_tac = Classical.slow_tac o addss; |
177 val slow_simp_tac = Classical.slow_tac o addss; |
182 val best_simp_tac = Classical.best_tac o addss; |
178 val best_simp_tac = Classical.best_tac o addss; |
|
179 |
|
180 |
183 |
181 |
184 (** concrete syntax **) |
182 (** concrete syntax **) |
185 |
183 |
186 (* attributes *) |
184 (* attributes *) |
187 |
185 |
219 |
217 |
220 (* theory setup *) |
218 (* theory setup *) |
221 |
219 |
222 val clasimp_setup = |
220 val clasimp_setup = |
223 Attrib.setup @{binding iff} iff_att "declaration of Simplifier / Classical rules" #> |
221 Attrib.setup @{binding iff} iff_att "declaration of Simplifier / Classical rules" #> |
224 Method.setup @{binding fastsimp} (clasimp_method' fast_simp_tac) "combined fast and simp (legacy name)" #> |
|
225 Method.setup @{binding fastforce} (clasimp_method' fast_force_tac) "combined fast and simp" #> |
222 Method.setup @{binding fastforce} (clasimp_method' fast_force_tac) "combined fast and simp" #> |
226 Method.setup @{binding slowsimp} (clasimp_method' slow_simp_tac) "combined slow and simp" #> |
223 Method.setup @{binding slowsimp} (clasimp_method' slow_simp_tac) "combined slow and simp" #> |
227 Method.setup @{binding bestsimp} (clasimp_method' best_simp_tac) "combined best and simp" #> |
224 Method.setup @{binding bestsimp} (clasimp_method' best_simp_tac) "combined best and simp" #> |
228 Method.setup @{binding force} (clasimp_method' force_tac) "force" #> |
225 Method.setup @{binding force} (clasimp_method' force_tac) "force" #> |
229 Method.setup @{binding auto} auto_method "auto" #> |
226 Method.setup @{binding auto} auto_method "auto" #> |