src/HOL/Tools/try.ML
Tue, 02 Nov 2010 20:55:12 +0100 wenzelm simplified some time constants;
Wed, 27 Oct 2010 19:14:33 +0200 blanchet reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
Mon, 25 Oct 2010 21:06:56 +0200 wenzelm renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
Fri, 22 Oct 2010 18:24:10 +0200 blanchet handle timeouts (to prevent failure from other threads);
Mon, 27 Sep 2010 09:17:24 +0200 blanchet comment out Auto Try until issues are resolved (automatically on by default even though the code says off; thread that continues in the background)
Wed, 22 Sep 2010 18:21:48 +0200 wenzelm renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
Fri, 17 Sep 2010 17:02:34 +0200 blanchet reorder proof methods and take out "best";
Mon, 13 Sep 2010 14:28:25 +0200 blanchet change signature of "Try.invoke_try" to make it more flexible
Mon, 13 Sep 2010 09:36:34 +0200 blanchet no timeout for Auto Try, since the Auto Tools framework takes care of timeouts
Sat, 11 Sep 2010 16:41:15 +0200 blanchet add Proof General option
Sat, 11 Sep 2010 16:39:54 +0200 blanchet make Try's output more concise
Sat, 11 Sep 2010 16:36:23 +0200 blanchet added Auto Try to the mix of automatic tools
Wed, 08 Sep 2010 15:57:50 +0200 blanchet remove "safe" (as suggested by Tobias) and added "arith" to "try"
Tue, 31 Aug 2010 21:17:19 +0200 blanchet distinguish between "by" and "apply"
Tue, 31 Aug 2010 21:01:47 +0200 blanchet fiddling with "try"
Tue, 31 Aug 2010 20:24:28 +0200 blanchet "try" -- a new diagnosis tool that tries to apply several methods in parallel
less more (0) tip