src/HOL/Tools/try.ML
2010-12-06 blanchet 2010-12-06 quiet Metis in "try"
2010-12-03 blanchet 2010-12-03 run synchronous Auto Tools in parallel
2010-11-02 wenzelm 2010-11-02 simplified some time constants;
2010-10-27 blanchet 2010-10-27 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)
2010-10-25 wenzelm 2010-10-25 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
2010-10-22 blanchet 2010-10-22 handle timeouts (to prevent failure from other threads); removed needless functions; added "metis" to the mix
2010-09-27 blanchet 2010-09-27 comment out Auto Try until issues are resolved (automatically on by default even though the code says off; thread that continues in the background)
2010-09-22 wenzelm 2010-09-22 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
2010-09-17 blanchet 2010-09-17 reorder proof methods and take out "best"; suggestions from Tobias
2010-09-13 blanchet 2010-09-13 change signature of "Try.invoke_try" to make it more flexible
2010-09-13 blanchet 2010-09-13 no timeout for Auto Try, since the Auto Tools framework takes care of timeouts
2010-09-11 blanchet 2010-09-11 add Proof General option
2010-09-11 blanchet 2010-09-11 make Try's output more concise
2010-09-11 blanchet 2010-09-11 added Auto Try to the mix of automatic tools
2010-09-08 blanchet 2010-09-08 remove "safe" (as suggested by Tobias) and added "arith" to "try"
2010-08-31 blanchet 2010-08-31 distinguish between "by" and "apply"
2010-08-31 blanchet 2010-08-31 fiddling with "try"
2010-08-31 blanchet 2010-08-31 "try" -- a new diagnosis tool that tries to apply several methods in parallel