411 || (parse_fact_refs >> only_relevance_override) |
411 || (parse_fact_refs >> only_relevance_override) |
412 val parse_relevance_override = |
412 val parse_relevance_override = |
413 Scan.optional (Args.parens (Scan.repeat parse_relevance_chunk |
413 Scan.optional (Args.parens (Scan.repeat parse_relevance_chunk |
414 >> merge_relevance_overrides)) |
414 >> merge_relevance_overrides)) |
415 no_relevance_override |
415 no_relevance_override |
416 val parse_sledgehammer_command = |
|
417 (Scan.optional Parse.short_ident runN -- parse_params |
|
418 -- parse_relevance_override -- Scan.option Parse.nat) #>> sledgehammer_trans |
|
419 val parse_sledgehammer_params_command = |
|
420 parse_params #>> sledgehammer_params_trans |
|
421 |
416 |
422 val _ = |
417 val _ = |
423 Outer_Syntax.improper_command sledgehammerN |
418 Outer_Syntax.improper_command @{command_spec "sledgehammer"} |
424 "search for first-order proof using automatic theorem provers" Keyword.diag |
419 "search for first-order proof using automatic theorem provers" |
425 parse_sledgehammer_command |
420 ((Scan.optional Parse.short_ident runN -- parse_params |
|
421 -- parse_relevance_override -- Scan.option Parse.nat) #>> sledgehammer_trans) |
426 val _ = |
422 val _ = |
427 Outer_Syntax.command sledgehammer_paramsN |
423 Outer_Syntax.command @{command_spec "sledgehammer_params"} |
428 "set and display the default parameters for Sledgehammer" Keyword.thy_decl |
424 "set and display the default parameters for Sledgehammer" |
429 parse_sledgehammer_params_command |
425 (parse_params #>> sledgehammer_params_trans) |
430 |
426 |
431 fun try_sledgehammer auto state = |
427 fun try_sledgehammer auto state = |
432 let |
428 let |
433 val ctxt = Proof.context_of state |
429 val ctxt = Proof.context_of state |
434 val mode = if auto then Auto_Try else Try |
430 val mode = if auto then Auto_Try else Try |