# HG changeset patch # User wenzelm # Date 1259079573 -3600 # Node ID 4328de748fb2ceffe4ad5a6d5fbf3347f6aecfa6 # Parent 4e0da333f75bcc6f0a05fc2f2d9353075fac1e82 some rearangement of load order to keep preferences adjacent -- slightly fragile; diff -r 4e0da333f75b -r 4328de748fb2 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Tue Nov 24 16:11:50 2009 +0100 +++ b/src/HOL/HOL.thy Tue Nov 24 17:19:33 2009 +0100 @@ -8,7 +8,6 @@ imports Pure "~~/src/Tools/Code_Generator" uses ("Tools/hologic.ML") - "~~/src/Tools/auto_solve.ML" "~~/src/Tools/IsaPlanner/zipper.ML" "~~/src/Tools/IsaPlanner/isand.ML" "~~/src/Tools/IsaPlanner/rw_tools.ML" diff -r 4e0da333f75b -r 4328de748fb2 src/Tools/Code_Generator.thy --- a/src/Tools/Code_Generator.thy Tue Nov 24 16:11:50 2009 +0100 +++ b/src/Tools/Code_Generator.thy Tue Nov 24 17:19:33 2009 +0100 @@ -7,9 +7,10 @@ theory Code_Generator imports Pure uses + "~~/src/Tools/auto_solve.ML" "~~/src/Tools/auto_counterexample.ML" + "~~/src/Tools/quickcheck.ML" "~~/src/Tools/value.ML" - "~~/src/Tools/quickcheck.ML" "~~/src/Tools/Code/code_preproc.ML" "~~/src/Tools/Code/code_thingol.ML" "~~/src/Tools/Code/code_printer.ML" diff -r 4e0da333f75b -r 4328de748fb2 src/Tools/auto_solve.ML --- a/src/Tools/auto_solve.ML Tue Nov 24 16:11:50 2009 +0100 +++ b/src/Tools/auto_solve.ML Tue Nov 24 17:19:33 2009 +0100 @@ -27,17 +27,17 @@ val _ = ProofGeneralPgip.add_preference Preferences.category_tracing + (Preferences.nat_pref auto_time_limit + "auto-solve-time-limit" + "Time limit for seeking automatic solutions (in milliseconds)."); + +val _ = + ProofGeneralPgip.add_preference Preferences.category_tracing (setmp_CRITICAL auto true (fn () => Preferences.bool_pref auto "auto-solve" "Try to solve newly declared lemmas with existing theorems.") ()); -val _ = - ProofGeneralPgip.add_preference Preferences.category_tracing - (Preferences.nat_pref auto_time_limit - "auto-solve-time-limit" - "Time limit for seeking automatic solutions (in milliseconds)."); - (* hook *)