# HG changeset patch
# User blanchet
# Date 1284193724 -7200
# Node ID ce5c6a8b03599d83e61541b7c2f889e095ec6da6
# Parent  80420a0f21797d917cca3bbe47db1a09504753e1
start renaming "Auto_Counterexample" to "Auto_Tools";
Auto Sledgehammer now uses so the name is clearly wrong

diff -r 80420a0f2179 -r ce5c6a8b0359 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sat Sep 11 10:25:27 2010 +0200
+++ b/src/HOL/IsaMakefile	Sat Sep 11 10:28:44 2010 +0200
@@ -122,8 +122,8 @@
   $(SRC)/Tools/IsaPlanner/rw_tools.ML \
   $(SRC)/Tools/IsaPlanner/zipper.ML \
   $(SRC)/Tools/atomize_elim.ML \
-  $(SRC)/Tools/auto_counterexample.ML \
   $(SRC)/Tools/auto_solve.ML \
+  $(SRC)/Tools/auto_tools.ML \
   $(SRC)/Tools/coherent.ML \
   $(SRC)/Tools/cong_tac.ML \
   $(SRC)/Tools/eqsubst.ML \
diff -r 80420a0f2179 -r ce5c6a8b0359 src/Tools/Code_Generator.thy
--- a/src/Tools/Code_Generator.thy	Sat Sep 11 10:25:27 2010 +0200
+++ b/src/Tools/Code_Generator.thy	Sat Sep 11 10:28:44 2010 +0200
@@ -8,8 +8,8 @@
 imports Pure
 uses
   "~~/src/Tools/cache_io.ML"
+  "~~/src/Tools/auto_tools.ML"
   "~~/src/Tools/auto_solve.ML"
-  "~~/src/Tools/auto_counterexample.ML"
   "~~/src/Tools/quickcheck.ML"
   "~~/src/Tools/value.ML"
   "~~/src/Tools/Code/code_preproc.ML" 
diff -r 80420a0f2179 -r ce5c6a8b0359 src/Tools/auto_counterexample.ML
--- a/src/Tools/auto_counterexample.ML	Sat Sep 11 10:25:27 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-(*  Title:      Tools/auto_counterexample.ML
-    Author:     Jasmin Blanchette, TU Muenchen
-
-Counterexample Search Unit (do not abbreviate!).
-*)
-
-signature AUTO_COUNTEREXAMPLE =
-sig
-  val time_limit: int Unsynchronized.ref
-
-  val register_tool :
-    string * (Proof.state -> bool * Proof.state) -> theory -> theory
-end;
-
-structure Auto_Counterexample : AUTO_COUNTEREXAMPLE =
-struct
-
-(* preferences *)
-
-val time_limit = Unsynchronized.ref 2500
-
-val _ =
-  ProofGeneralPgip.add_preference Preferences.category_tracing
-    (Preferences.nat_pref time_limit
-      "auto-counterexample-time-limit"
-      "Time limit for automatic counterexample search (in milliseconds).")
-
-
-(* configuration *)
-
-structure Data = Theory_Data
-(
-  type T = (string * (Proof.state -> bool * Proof.state)) list
-  val empty = []
-  val extend = I
-  fun merge data : T = AList.merge (op =) (K true) data
-)
-
-val register_tool = Data.map o AList.update (op =)
-
-
-(* automatic testing *)
-
-val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
-  case !time_limit of
-    0 => state
-  | ms =>
-    TimeLimit.timeLimit (Time.fromMilliseconds ms)
-        (fn () =>
-            if interact andalso not (!Toplevel.quiet) then
-              fold_rev (fn (_, tool) => fn (true, state) => (true, state)
-                                         | (false, state) => tool state)
-                   (Data.get (Proof.theory_of state)) (false, state) |> snd
-            else
-              state) ()
-    handle TimeLimit.TimeOut =>
-           (warning "Automatic counterexample search timed out."; state)))
-
-end;
diff -r 80420a0f2179 -r ce5c6a8b0359 src/Tools/auto_tools.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/auto_tools.ML	Sat Sep 11 10:28:44 2010 +0200
@@ -0,0 +1,59 @@
+(*  Title:      Tools/auto_counterexample.ML
+    Author:     Jasmin Blanchette, TU Muenchen
+
+Counterexample Search Unit (do not abbreviate!).
+*)
+
+signature AUTO_COUNTEREXAMPLE =
+sig
+  val time_limit: int Unsynchronized.ref
+
+  val register_tool :
+    string * (Proof.state -> bool * Proof.state) -> theory -> theory
+end;
+
+structure Auto_Counterexample : AUTO_COUNTEREXAMPLE =
+struct
+
+(* preferences *)
+
+val time_limit = Unsynchronized.ref 2500
+
+val _ =
+  ProofGeneralPgip.add_preference Preferences.category_tracing
+    (Preferences.nat_pref time_limit
+      "auto-counterexample-time-limit"
+      "Time limit for automatic counterexample search (in milliseconds).")
+
+
+(* configuration *)
+
+structure Data = Theory_Data
+(
+  type T = (string * (Proof.state -> bool * Proof.state)) list
+  val empty = []
+  val extend = I
+  fun merge data : T = AList.merge (op =) (K true) data
+)
+
+val register_tool = Data.map o AList.update (op =)
+
+
+(* automatic testing *)
+
+val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
+  case !time_limit of
+    0 => state
+  | ms =>
+    TimeLimit.timeLimit (Time.fromMilliseconds ms)
+        (fn () =>
+            if interact andalso not (!Toplevel.quiet) then
+              fold_rev (fn (_, tool) => fn (true, state) => (true, state)
+                                         | (false, state) => tool state)
+                   (Data.get (Proof.theory_of state)) (false, state) |> snd
+            else
+              state) ()
+    handle TimeLimit.TimeOut =>
+           (warning "Automatic counterexample search timed out."; state)))
+
+end;