equal
deleted
inserted
replaced
2967 val _ = |
2967 val _ = |
2968 Outer_Syntax.command @{command_keyword refute} |
2968 Outer_Syntax.command @{command_keyword refute} |
2969 "try to find a model that refutes a given subgoal" |
2969 "try to find a model that refutes a given subgoal" |
2970 (scan_parms -- Scan.optional Parse.nat 1 >> |
2970 (scan_parms -- Scan.optional Parse.nat 1 >> |
2971 (fn (parms, i) => |
2971 (fn (parms, i) => |
2972 Toplevel.keep (fn state => |
2972 Toplevel.keep_proof (fn state => |
2973 let |
2973 let |
2974 val ctxt = Toplevel.context_of state; |
2974 val ctxt = Toplevel.context_of state; |
2975 val {goal = st, ...} = Proof.raw_goal (Toplevel.proof_of state); |
2975 val {goal = st, ...} = Proof.raw_goal (Toplevel.proof_of state); |
2976 in refute_goal ctxt parms st i; () end))); |
2976 in refute_goal ctxt parms st i; () end))); |
2977 |
2977 |