Thu, 29 Nov 2012 14:29:29 +0100 wenzelm merged
Thu, 29 Nov 2012 09:59:20 +0100 hoelzl make SML/NJ happy (give names for all fields in a record)
Thu, 29 Nov 2012 14:05:53 +0100 wenzelm more robust syntax that survives collapse of \<^isub> and \<^sub>;
Thu, 29 Nov 2012 10:56:59 +0100 wenzelm further update and clarification of the all-important README_REPOSITORY;
Thu, 29 Nov 2012 10:45:25 +0100 wenzelm more uniform ML statistics;
Wed, 28 Nov 2012 19:19:39 +0100 wenzelm merged
Wed, 28 Nov 2012 12:25:43 +0100 smolkas improved readability
Wed, 28 Nov 2012 12:25:43 +0100 smolkas tweaked calculation of sledgehammer messages
Wed, 28 Nov 2012 12:25:43 +0100 smolkas adapted sledgehammer warnings
Wed, 28 Nov 2012 12:25:43 +0100 smolkas fixed case split preplaying
Wed, 28 Nov 2012 12:25:43 +0100 smolkas fixed preplaying of case splits; incorperated new name of structure: Isabelle_Markup -> Markup
Wed, 28 Nov 2012 12:25:43 +0100 smolkas preplay case splits
Wed, 28 Nov 2012 12:25:43 +0100 smolkas added warning when shrinking proof without preplaying
Wed, 28 Nov 2012 12:25:43 +0100 smolkas deal with the case that metis does not time out, but fails instead
Wed, 28 Nov 2012 12:25:43 +0100 smolkas reapplied changes to make SML/NJ happy
Wed, 28 Nov 2012 12:25:43 +0100 smolkas renaming, minor tweaks, added signature
Wed, 28 Nov 2012 12:25:43 +0100 smolkas added signature
Wed, 28 Nov 2012 12:25:43 +0100 smolkas moved thms_of_name to Sledgehammer_Util and removed copies, updated references
Wed, 28 Nov 2012 12:25:43 +0100 smolkas removed duplicate decleration
Wed, 28 Nov 2012 12:25:43 +0100 smolkas made use of sledgehammer_util
Wed, 28 Nov 2012 12:25:43 +0100 smolkas renamed sledgehammer_isar_reconstruct to sledgehammer_proof
Wed, 28 Nov 2012 12:25:43 +0100 smolkas added comments to new source files
Wed, 28 Nov 2012 12:25:43 +0100 smolkas fixed problem with fact names
Wed, 28 Nov 2012 12:25:06 +0100 smolkas remove hack and generalize code slightly
Wed, 28 Nov 2012 12:23:44 +0100 smolkas simplified isar_qualifiers and qs merging
Wed, 28 Nov 2012 12:22:17 +0100 smolkas put shrink in own structure
Wed, 28 Nov 2012 12:22:05 +0100 smolkas put annotate in own structure
Wed, 28 Nov 2012 12:21:42 +0100 smolkas support assumptions as facts for preplaying
Wed, 28 Nov 2012 12:20:06 +0100 smolkas some minor improvements in shrink_proof
Wed, 28 Nov 2012 17:18:53 +0100 wenzelm some support for ML runtime statistics;
Wed, 28 Nov 2012 16:09:05 +0100 wenzelm prefer tight Markup.print_int/parse_int for property values;
Wed, 28 Nov 2012 16:07:17 +0100 wenzelm clarified new identifier syntax: exclude \<^isup>, include subscripted prime (to allow imitating full identifier here);
Wed, 28 Nov 2012 15:59:18 +0100 wenzelm eliminated slightly odd identifiers;
Wed, 28 Nov 2012 15:38:12 +0100 wenzelm tuned syntax, potentially more robust;
Wed, 28 Nov 2012 14:55:46 +0100 wenzelm smarter list layout;
Tue, 27 Nov 2012 20:01:57 +0100 wenzelm repaired text following 491c5c81c2e8;
Tue, 27 Nov 2012 19:43:00 +0100 wenzelm merged
Tue, 27 Nov 2012 19:31:11 +0100 hoelzl introduce filter_lim as a generatlization of tendsto
Tue, 27 Nov 2012 19:24:30 +0100 wenzelm merged
Tue, 27 Nov 2012 13:48:40 +0100 immler based countable topological basis on Countable_Set
Tue, 27 Nov 2012 11:29:47 +0100 immler qualified interpretation of sigma_algebra, to avoid name clashes
Thu, 22 Nov 2012 10:09:54 +0100 immler eliminated finite_set_sequence with countable set
Tue, 27 Nov 2012 19:22:36 +0100 wenzelm support for sub-structured identifier syntax (inactive);
Tue, 27 Nov 2012 13:22:29 +0100 wenzelm eliminated some improper identifiers;
Tue, 27 Nov 2012 10:56:31 +0100 hoelzl add upper bounds for factorial and binomial; add equation for binomial using nat-division (both from AFP/Girth_Chromatic)
Mon, 26 Nov 2012 21:46:04 +0100 wenzelm tuned signature;
Mon, 26 Nov 2012 21:10:42 +0100 wenzelm more uniform Symbol.is_ascii_identifier in ML/Scala;
Mon, 26 Nov 2012 20:58:41 +0100 wenzelm tuned;
Mon, 26 Nov 2012 20:39:19 +0100 wenzelm clarified Symbol.scan_ascii_id;
Mon, 26 Nov 2012 20:29:40 +0100 wenzelm tuned;
Mon, 26 Nov 2012 20:09:51 +0100 wenzelm convenience operations for table as set;
Mon, 26 Nov 2012 19:56:09 +0100 wenzelm removed remains of Oheimb's double-space (cf. 0a5af667dc75);
Mon, 26 Nov 2012 19:53:43 +0100 wenzelm tuned;
Mon, 26 Nov 2012 17:13:44 +0100 wenzelm merged
Mon, 26 Nov 2012 16:01:04 +0100 blanchet updated two components
Mon, 26 Nov 2012 15:31:03 +0100 blanchet simplify code slightly
Mon, 26 Nov 2012 15:31:03 +0100 blanchet avoid non-ASCII sign
Mon, 26 Nov 2012 14:20:51 +0100 kuncar generate a parameterized correspondence relation
Mon, 26 Nov 2012 14:20:36 +0100 kuncar quot_thm_crel
Mon, 26 Nov 2012 14:15:48 +0100 kuncar add option_fold
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip