--- a/src/HOL/Tools/refute.ML Thu Sep 02 16:45:21 2010 +0200
+++ b/src/HOL/Tools/refute.ML Thu Sep 02 17:12:16 2010 +0200
@@ -3257,5 +3257,47 @@
add_printer "stlc" stlc_printer #>
add_printer "IDT" IDT_printer;
+
+
+(** outer syntax commands 'refute' and 'refute_params' **)
+
+(* argument parsing *)
+
+(*optional list of arguments of the form [name1=value1, name2=value2, ...]*)
+
+val scan_parm = Parse.name -- (Scan.optional (Parse.$$$ "=" |-- Parse.name) "true")
+val scan_parms = Scan.optional (Parse.$$$ "[" |-- Parse.list scan_parm --| Parse.$$$ "]") [];
+
+
+(* 'refute' command *)
+
+val _ =
+ Outer_Syntax.improper_command "refute"
+ "try to find a model that refutes a given subgoal" Keyword.diag
+ (scan_parms -- Scan.optional Parse.nat 1 >>
+ (fn (parms, i) =>
+ Toplevel.keep (fn state =>
+ let
+ val ctxt = Toplevel.context_of state;
+ val {goal = st, ...} = Proof.raw_goal (Toplevel.proof_of state);
+ in refute_goal ctxt parms st i end)));
+
+
+(* 'refute_params' command *)
+
+val _ =
+ Outer_Syntax.command "refute_params"
+ "show/store default parameters for the 'refute' command" Keyword.thy_decl
+ (scan_parms >> (fn parms =>
+ Toplevel.theory (fn thy =>
+ let
+ val thy' = fold set_default_param parms thy;
+ val output =
+ (case get_default_params thy' of
+ [] => "none"
+ | new_defaults => cat_lines (map (fn (x, y) => x ^ "=" ^ y) new_defaults));
+ val _ = writeln ("Default parameters for 'refute':\n" ^ output);
+ in thy' end)));
+
end;