--- a/src/HOL/IsaMakefile Thu Sep 02 16:45:21 2010 +0200
+++ b/src/HOL/IsaMakefile Thu Sep 02 17:12:16 2010 +0200
@@ -209,7 +209,6 @@
Tools/primrec.ML \
Tools/prop_logic.ML \
Tools/refute.ML \
- Tools/refute_isar.ML \
Tools/rewrite_hol_proof.ML \
Tools/sat_funcs.ML \
Tools/sat_solver.ML \
--- a/src/HOL/Refute.thy Thu Sep 02 16:45:21 2010 +0200
+++ b/src/HOL/Refute.thy Thu Sep 02 17:12:16 2010 +0200
@@ -9,9 +9,7 @@
theory Refute
imports Hilbert_Choice List
-uses
- "Tools/refute.ML"
- "Tools/refute_isar.ML"
+uses "Tools/refute.ML"
begin
setup Refute.setup
@@ -92,16 +90,14 @@
(* ------------------------------------------------------------------------- *)
(* FILES *)
(* *)
-(* HOL/Tools/prop_logic.ML Propositional logic *)
-(* HOL/Tools/sat_solver.ML SAT solvers *)
-(* HOL/Tools/refute.ML Translation HOL -> propositional logic and *)
-(* Boolean assignment -> HOL model *)
-(* HOL/Tools/refute_isar.ML Adds 'refute'/'refute_params' to Isabelle's *)
-(* syntax *)
-(* HOL/Refute.thy This file: loads the ML files, basic setup, *)
-(* documentation *)
-(* HOL/SAT.thy Sets default parameters *)
-(* HOL/ex/RefuteExamples.thy Examples *)
+(* HOL/Tools/prop_logic.ML Propositional logic *)
+(* HOL/Tools/sat_solver.ML SAT solvers *)
+(* HOL/Tools/refute.ML Translation HOL -> propositional logic and *)
+(* Boolean assignment -> HOL model *)
+(* HOL/Refute.thy This file: loads the ML files, basic setup, *)
+(* documentation *)
+(* HOL/SAT.thy Sets default parameters *)
+(* HOL/ex/Refute_Examples.thy Examples *)
(* ------------------------------------------------------------------------- *)
\end{verbatim}
*}
--- 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;
--- a/src/HOL/Tools/refute_isar.ML Thu Sep 02 16:45:21 2010 +0200
+++ b/src/HOL/Tools/refute_isar.ML Thu Sep 02 17:12:16 2010 +0200
@@ -2,49 +2,6 @@
Author: Tjark Weber
Copyright 2003-2007
-Outer syntax commands 'refute' and 'refute_params'.
-*)
-
-structure Refute_Isar: sig end =
-struct
-
-(* 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.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 Refute.set_default_param parms thy;
- val output =
- (case Refute.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;