Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
Tue, 10 Sep 2013 15:56:51 +0200 blanchet removed completely needless, inefficient code file | diff | annotate
Tue, 10 Sep 2013 15:56:51 +0200 blanchet minor speed optimization file | diff | annotate
Tue, 10 Sep 2013 15:56:51 +0200 blanchet got rid of another taboo that appears to make no difference in practice (and that slows down the relevance filter) file | diff | annotate
Tue, 10 Sep 2013 15:56:51 +0200 blanchet avoid double traversal of term file | diff | annotate
Tue, 10 Sep 2013 15:56:51 +0200 blanchet got rid of old, needless logic file | diff | annotate
Tue, 10 Sep 2013 15:56:51 +0200 blanchet faster uniquification file | diff | annotate
Tue, 10 Sep 2013 15:56:51 +0200 blanchet stronger fact normalization file | diff | annotate
Tue, 10 Sep 2013 15:56:51 +0200 blanchet gracefully handle huge thys file | diff | annotate
Tue, 10 Sep 2013 15:56:51 +0200 blanchet speed up detection of simp rules file | diff | annotate
Thu, 16 May 2013 13:34:13 +0200 blanchet tuning -- renamed '_from_' to '_of_' in Sledgehammer file | diff | annotate
Wed, 15 May 2013 17:43:42 +0200 blanchet renamed Sledgehammer functions with 'for' in their names to 'of' file | diff | annotate
Fri, 15 Feb 2013 11:47:33 +0100 haftmann systematic conversions between nat and nibble/char; file | diff | annotate
Thu, 14 Feb 2013 15:27:10 +0100 haftmann reform of predicate compiler / quickcheck theories: file | diff | annotate
Thu, 31 Jan 2013 17:54:05 +0100 blanchet distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds file | diff | annotate
Thu, 10 Jan 2013 23:34:20 +0100 blanchet make name table work the way it was intended to file | diff | annotate
Sun, 06 Jan 2013 17:38:29 +0100 blanchet put single-theorem names before multi-theorem ones (broken since 5d147d492792) file | diff | annotate
Sat, 05 Jan 2013 11:24:09 +0100 blanchet tuned blacklisting in relevance filter file | diff | annotate
Fri, 04 Jan 2013 21:56:20 +0100 blanchet refined class handling, to prevent cycles in fact graph file | diff | annotate
Fri, 04 Jan 2013 21:56:19 +0100 blanchet learn from low-level, inside-class facts file | diff | annotate
Fri, 04 Jan 2013 21:56:19 +0100 blanchet tuning file | diff | annotate
Mon, 17 Dec 2012 22:06:28 +0100 blanchet add a timeout in induction rule instantiation file | diff | annotate
Thu, 13 Dec 2012 23:47:01 +0100 blanchet get rid of some junk facts in the MaSh evaluation driver file | diff | annotate
Wed, 12 Dec 2012 21:48:29 +0100 blanchet tweaked which facts are included for MaSh evaluations file | diff | annotate
Wed, 12 Dec 2012 21:48:29 +0100 blanchet don't query blacklisted theorems in evaluation driver file | diff | annotate
Wed, 12 Dec 2012 21:48:29 +0100 blanchet export a pair of ML functions file | diff | annotate
Wed, 12 Dec 2012 15:38:47 +0100 blanchet further fix related to bd9a0028b063 -- that change was per se right, but it exposed a bug in the pattern for "all" file | diff | annotate
Wed, 12 Dec 2012 15:25:17 +0100 blanchet better tautology check -- don't reject "prod_cases3" for example file | diff | annotate
Wed, 12 Dec 2012 13:28:23 +0100 blanchet really all facts means really all facts (well, almost) file | diff | annotate
Wed, 12 Dec 2012 02:47:45 +0100 blanchet merge aliased theorems in MaSh dependencies, modulo symmetry of equality file | diff | annotate
Wed, 12 Dec 2012 00:14:58 +0100 blanchet push normalization further -- avoid theorems that are duplicates of each other except for equality symmetry (esp. for "list.distinct(1)" vs. "(2)" etc.) file | diff | annotate
Sat, 08 Dec 2012 21:54:28 +0100 blanchet don't blacklist "case" theorems -- this causes problems in MaSh later file | diff | annotate
Mon, 26 Nov 2012 21:46:04 +0100 wenzelm tuned signature; file | diff | annotate
Mon, 12 Nov 2012 14:46:42 +0100 blanchet fixed detection of tautologies -- things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies file | diff | annotate
Mon, 12 Nov 2012 12:06:56 +0100 blanchet avoid messing too much with output of "string_of_term", so that it doesn't break the yxml encoding for jEdit file | diff | annotate
Mon, 12 Nov 2012 11:52:37 +0100 blanchet centralized term printing code file | diff | annotate
Mon, 12 Nov 2012 11:32:22 +0100 blanchet thread context correctly when printing backquoted facts file | diff | annotate
Wed, 31 Oct 2012 11:23:21 +0100 blanchet tuning file | diff | annotate
Fri, 03 Aug 2012 17:56:35 +0200 blanchet rule out same "technical" theories for MePo as for MaSh file | diff | annotate
Thu, 26 Jul 2012 10:48:03 +0200 blanchet repaired accessibility chains generated by MaSh exporter + tuned one function out file | diff | annotate
Mon, 23 Jul 2012 15:32:30 +0200 blanchet identified "evil" theories for MaSh -- this is rather ad hoc, but so is MaSh anyway file | diff | annotate
Mon, 23 Jul 2012 15:32:30 +0200 blanchet distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh file | diff | annotate
Mon, 23 Jul 2012 15:32:30 +0200 blanchet tuning file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet honor suggested MaSh weights file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet minimal maxes + tuning file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet name tuning file | diff | annotate
Fri, 20 Jul 2012 22:19:46 +0200 blanchet fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully file | diff | annotate
Wed, 18 Jul 2012 08:44:05 +0200 blanchet optimize parent computation in MaSh + remove temporary files file | diff | annotate
Wed, 18 Jul 2012 08:44:04 +0200 blanchet don't include hidden facts in relevance filter + tweak MaSh learning file | diff | annotate
Wed, 18 Jul 2012 08:44:03 +0200 blanchet centrally construct expensive data structures file | diff | annotate
Wed, 18 Jul 2012 08:44:03 +0200 blanchet more work on MaSh file | diff | annotate
Wed, 18 Jul 2012 08:44:03 +0200 blanchet gracefully handle the case of empty theories when going up the accessibility chain file | diff | annotate
Wed, 18 Jul 2012 08:44:03 +0200 blanchet more code rationalization in relevance filter file | diff | annotate
Wed, 11 Jul 2012 21:43:19 +0200 blanchet moved most of MaSh exporter code to Sledgehammer file | diff | annotate
Wed, 11 Jul 2012 21:43:19 +0200 blanchet further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer) file | diff | annotate
less more (0) tip
isabelle