# HG changeset patch
# User blanchet
# Date 1284216075 -7200
# Node ID c277c79fb9db0eeb01bdba972e9ec613abe239b7
# Parent  538b94dc62de893266bc3a81a1c70f337cc0afa4
add Proof General option

diff -r 538b94dc62de -r c277c79fb9db src/HOL/Tools/try.ML
--- 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 =