equal
deleted
inserted
replaced
2965 |
2965 |
2966 |
2966 |
2967 (* 'refute' command *) |
2967 (* 'refute' command *) |
2968 |
2968 |
2969 val _ = |
2969 val _ = |
2970 Outer_Syntax.improper_command @{command_spec "refute"} |
2970 Outer_Syntax.command @{command_spec "refute"} |
2971 "try to find a model that refutes a given subgoal" |
2971 "try to find a model that refutes a given subgoal" |
2972 (scan_parms -- Scan.optional Parse.nat 1 >> |
2972 (scan_parms -- Scan.optional Parse.nat 1 >> |
2973 (fn (parms, i) => |
2973 (fn (parms, i) => |
2974 Toplevel.unknown_proof o |
2974 Toplevel.unknown_proof o |
2975 Toplevel.keep (fn state => |
2975 Toplevel.keep (fn state => |