Mon, 27 Jun 2011 22:44:44 +0200 wenzelm merged
Mon, 27 Jun 2011 17:04:04 +0200 krauss new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
Mon, 27 Jun 2011 14:56:39 +0200 blanchet added reference for MESON
Mon, 27 Jun 2011 14:56:37 +0200 blanchet document "meson" and "metis" in HOL specific section of the Isar ref manual
Mon, 27 Jun 2011 14:56:35 +0200 blanchet clarify minimizer output
Mon, 27 Jun 2011 14:56:33 +0200 blanchet don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
Mon, 27 Jun 2011 14:56:32 +0200 blanchet tweaked comment
Mon, 27 Jun 2011 14:56:31 +0200 blanchet document "sound" option
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -8 +8 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip