wenzelm [Thu, 29 Nov 2012 17:12:51 +0100] rev 50287
simplified use of fold/map;
tuned;
wenzelm [Thu, 29 Nov 2012 16:59:53 +0100] rev 50286
tuned;
wenzelm [Thu, 29 Nov 2012 16:52:13 +0100] rev 50285
prefer 32 bit platform for ISABELLE_FULL_TEST, to make memory problems more explicit instead of disk thrashing (notably in HOL-Quickcheck_Benchmark);
wenzelm [Thu, 29 Nov 2012 14:29:29 +0100] rev 50284
merged
hoelzl [Thu, 29 Nov 2012 09:59:20 +0100] rev 50283
make SML/NJ happy (give names for all fields in a record)
wenzelm [Thu, 29 Nov 2012 14:05:53 +0100] rev 50282
more robust syntax that survives collapse of \<^isub> and \<^sub>;
wenzelm [Thu, 29 Nov 2012 10:56:59 +0100] rev 50281
further update and clarification of the all-important README_REPOSITORY;
wenzelm [Thu, 29 Nov 2012 10:45:25 +0100] rev 50280
more uniform ML statistics;
wenzelm [Wed, 28 Nov 2012 19:19:39 +0100] rev 50279
merged
smolkas [Wed, 28 Nov 2012 12:25:43 +0100] rev 50278
improved readability
smolkas [Wed, 28 Nov 2012 12:25:43 +0100] rev 50277
tweaked calculation of sledgehammer messages
smolkas [Wed, 28 Nov 2012 12:25:43 +0100] rev 50276
adapted sledgehammer warnings
smolkas [Wed, 28 Nov 2012 12:25:43 +0100] rev 50275
fixed case split preplaying
smolkas [Wed, 28 Nov 2012 12:25:43 +0100] rev 50274
fixed preplaying of case splits; incorperated new name of structure: Isabelle_Markup -> Markup
smolkas [Wed, 28 Nov 2012 12:25:43 +0100] rev 50273
preplay case splits
smolkas [Wed, 28 Nov 2012 12:25:43 +0100] rev 50272
added warning when shrinking proof without preplaying
smolkas [Wed, 28 Nov 2012 12:25:43 +0100] rev 50271
deal with the case that metis does not time out, but fails instead
smolkas [Wed, 28 Nov 2012 12:25:43 +0100] rev 50270
reapplied changes to make SML/NJ happy
smolkas [Wed, 28 Nov 2012 12:25:43 +0100] rev 50269
renaming, minor tweaks, added signature
smolkas [Wed, 28 Nov 2012 12:25:43 +0100] rev 50268
added signature
smolkas [Wed, 28 Nov 2012 12:25:43 +0100] rev 50267
moved thms_of_name to Sledgehammer_Util and removed copies, updated references
smolkas [Wed, 28 Nov 2012 12:25:43 +0100] rev 50266
removed duplicate decleration
smolkas [Wed, 28 Nov 2012 12:25:43 +0100] rev 50265
made use of sledgehammer_util
smolkas [Wed, 28 Nov 2012 12:25:43 +0100] rev 50264
renamed sledgehammer_isar_reconstruct to sledgehammer_proof
smolkas [Wed, 28 Nov 2012 12:25:43 +0100] rev 50263
added comments to new source files
smolkas [Wed, 28 Nov 2012 12:25:43 +0100] rev 50262
fixed problem with fact names
smolkas [Wed, 28 Nov 2012 12:25:06 +0100] rev 50261
remove hack and generalize code slightly
smolkas [Wed, 28 Nov 2012 12:23:44 +0100] rev 50260
simplified isar_qualifiers and qs merging
smolkas [Wed, 28 Nov 2012 12:22:17 +0100] rev 50259
put shrink in own structure
smolkas [Wed, 28 Nov 2012 12:22:05 +0100] rev 50258
put annotate in own structure