equal
deleted
inserted
replaced
75 |> tap (fn NONE => writeln "Tried in vain." | _ => ()) |
75 |> tap (fn NONE => writeln "Tried in vain." | _ => ()) |
76 |
76 |
77 val _ = |
77 val _ = |
78 Outer_Syntax.command @{command_keyword try} |
78 Outer_Syntax.command @{command_keyword try} |
79 "try a combination of automatic proving and disproving tools" |
79 "try a combination of automatic proving and disproving tools" |
80 (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of))) |
80 (Scan.succeed (Toplevel.keep_proof (ignore o try_tools o Toplevel.proof_of))) |
81 |
81 |
82 |
82 |
83 (* automatic try (TTY) *) |
83 (* automatic try (TTY) *) |
84 |
84 |
85 fun auto_try state = |
85 fun auto_try state = |