186 val recdef_congN = "recdef_cong"; |
186 val recdef_congN = "recdef_cong"; |
187 val recdef_wfN = "recdef_wf"; |
187 val recdef_wfN = "recdef_wf"; |
188 |
188 |
189 val recdef_modifiers = |
189 val recdef_modifiers = |
190 [Args.$$$ recdef_simpN -- Args.colon >> K ((I, simp_add_local): Method.modifier), |
190 [Args.$$$ recdef_simpN -- Args.colon >> K ((I, simp_add_local): Method.modifier), |
191 Args.$$$ recdef_simpN -- Args.$$$ Args.addN -- Args.colon >> K (I, simp_add_local), |
191 Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (I, simp_add_local), |
192 Args.$$$ recdef_simpN -- Args.$$$ Args.delN -- Args.colon >> K (I, simp_del_local), |
192 Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (I, simp_del_local), |
193 Args.$$$ recdef_congN -- Args.colon >> K (I, cong_add_local), |
193 Args.$$$ recdef_congN -- Args.colon >> K (I, cong_add_local), |
194 Args.$$$ recdef_congN -- Args.$$$ Args.addN -- Args.colon >> K (I, cong_add_local), |
194 Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (I, cong_add_local), |
195 Args.$$$ recdef_congN -- Args.$$$ Args.delN -- Args.colon >> K (I, cong_del_local), |
195 Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (I, cong_del_local), |
196 Args.$$$ recdef_wfN -- Args.colon >> K (I, wf_add_local), |
196 Args.$$$ recdef_wfN -- Args.colon >> K (I, wf_add_local), |
197 Args.$$$ recdef_wfN -- Args.$$$ Args.addN -- Args.colon >> K (I, wf_add_local), |
197 Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (I, wf_add_local), |
198 Args.$$$ recdef_wfN -- Args.$$$ Args.delN -- Args.colon >> K (I, wf_del_local)] @ |
198 Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (I, wf_del_local)] @ |
199 Clasimp.clasimp_modifiers; |
199 Clasimp.clasimp_modifiers; |
200 |
200 |
201 |
201 |
202 |
202 |
203 (** prepare_hints(_i) **) |
203 (** prepare_hints(_i) **) |