equal
deleted
inserted
replaced
417 else |
417 else |
418 error ("Unknown subcommand: " ^ quote subcommand ^ ".") |
418 error ("Unknown subcommand: " ^ quote subcommand ^ ".") |
419 end |
419 end |
420 |
420 |
421 fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) = |
421 fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) = |
|
422 Toplevel.unknown_proof o |
422 Toplevel.keep (hammer_away params subcommand opt_i fact_override |
423 Toplevel.keep (hammer_away params subcommand opt_i fact_override |
423 o Toplevel.proof_of) |
424 o Toplevel.proof_of) |
424 |
425 |
425 fun string_for_raw_param (name, value) = name ^ " = " ^ implode_param value |
426 fun string_for_raw_param (name, value) = name ^ " = " ^ implode_param value |
426 |
427 |