equal
deleted
inserted
replaced
224 | NONE => dummy |
224 | NONE => dummy |
225 end |
225 end |
226 *} |
226 *} |
227 |
227 |
228 ML {* |
228 ML {* |
229 fun gen_eval_method conv = Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' |
229 fun gen_eval_method conv = Method.ctxt_args (fn ctxt => SIMPLE_METHOD' |
230 (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt) |
230 (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt) |
231 THEN' rtac TrueI)) |
231 THEN' rtac TrueI)) |
232 *} |
232 *} |
233 |
233 |
234 method_setup eval = {* gen_eval_method eval_oracle *} |
234 method_setup eval = {* gen_eval_method eval_oracle *} |
235 "solve goal by evaluation" |
235 "solve goal by evaluation" |
236 |
236 |
237 method_setup evaluation = {* gen_eval_method Codegen.evaluation_conv *} |
237 method_setup evaluation = {* gen_eval_method Codegen.evaluation_conv *} |
238 "solve goal by evaluation" |
238 "solve goal by evaluation" |
239 |
239 |
240 method_setup normalization = {* (Method.no_args o Method.SIMPLE_METHOD') |
240 method_setup normalization = {* (Method.no_args o SIMPLE_METHOD') |
241 (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k))) |
241 (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k))) |
242 *} "solve goal by normalization" |
242 *} "solve goal by normalization" |
243 |
243 |
244 |
244 |
245 subsection {* Quickcheck *} |
245 subsection {* Quickcheck *} |