author | blanchet |
Sat, 11 Sep 2010 16:41:15 +0200 | |
changeset 39333 | c277c79fb9db |
parent 39332 | 538b94dc62de |
child 39334 | c0bb925ae912 |
--- a/src/HOL/Tools/try.ML Sat Sep 11 16:39:54 2010 +0200 +++ b/src/HOL/Tools/try.ML Sat Sep 11 16:41:15 2010 +0200 @@ -16,6 +16,12 @@ val auto = Unsynchronized.ref false +val _ = + ProofGeneralPgip.add_preference Preferences.category_tracing + (setmp_noncritical auto true (fn () => + Preferences.bool_pref auto + "auto-try" "Try standard proof methods.") ()); + val timeout = Time.fromSeconds 5 fun can_apply pre post tac st =