Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/TPTP/atp_theory_export.ML
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2}; file | diff | annotate
Thu, 06 Nov 2014 15:42:34 +0100 wenzelm proper Keyword.keywords (cf. 82a71046dce8); file | diff | annotate
Fri, 25 Jul 2014 12:22:18 +0200 blanchet compile file | diff | annotate
Tue, 24 Jun 2014 15:49:20 +0200 blanchet tuning file | diff | annotate
Tue, 24 Jun 2014 15:08:19 +0200 blanchet optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct) file | diff | annotate
Mon, 16 Jun 2014 19:44:02 +0200 blanchet compile file | diff | annotate
Tue, 17 Dec 2013 14:03:29 +0100 blanchet primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype) file | diff | annotate
Thu, 24 Oct 2013 12:43:33 +0200 blanchet use definitions for LEO-II as well -- this simplifies the code and matches some users' expectations file | diff | annotate
Sun, 29 Sep 2013 12:21:11 +0200 wenzelm made SML/NJ happy (NB: toplevel ML environment is unmanaged); file | diff | annotate
Thu, 12 Sep 2013 22:10:57 +0200 blanchet prefixed types and some functions with "atp_" for disambiguation file | diff | annotate
Tue, 13 Aug 2013 10:26:56 +0200 blanchet Vampire 3.0 requires types to be declared -- make it happy (and get rid of "implicit" types since only Satallax seems to support them anymore) file | diff | annotate
Mon, 29 Jul 2013 15:30:31 +0200 blanchet added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram") 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
Tue, 09 Apr 2013 16:32:04 +0200 blanchet handle case clashes on Mac file system by encoding goal numbers file | diff | annotate
Tue, 09 Apr 2013 15:19:14 +0200 blanchet smoothly handle cyclic graphs file | diff | annotate
Tue, 09 Apr 2013 15:19:14 +0200 blanchet compile + fixed naming convention file | diff | annotate
Tue, 09 Apr 2013 15:19:14 +0200 blanchet no need to filter tautologies anymore -- they are prefiltered by "all_facts"' file | diff | annotate
Tue, 09 Apr 2013 15:19:14 +0200 blanchet work on CASC LTB ISA exporter file | diff | annotate
Mon, 08 Apr 2013 14:16:00 +0200 blanchet try to preserve original linearization file | diff | annotate
Mon, 08 Apr 2013 12:27:13 +0200 blanchet use somewhat lighter encoding file | diff | annotate
Thu, 17 Jan 2013 14:01:45 +0100 blanchet added E-Par support file | diff | annotate
Fri, 04 Jan 2013 21:56:20 +0100 blanchet refined class handling, to prevent cycles in fact graph file | diff | annotate
Thu, 13 Dec 2012 22:49:08 +0100 blanchet generate comments with original names for debugging 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
Sat, 08 Dec 2012 21:54:28 +0100 blanchet don't blacklist "case" theorems -- this causes problems in MaSh later file | diff | annotate
Tue, 07 Aug 2012 14:29:18 +0200 blanchet stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users 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 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh 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 fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully file | diff | annotate
Fri, 20 Jul 2012 22:19:45 +0200 blanchet renamed ML structures file | diff | annotate
Fri, 20 Jul 2012 22:19:45 +0200 blanchet use "eproof_ram" script if available (plug-in replacement for "eproof", but faster) file | diff | annotate
Wed, 18 Jul 2012 08:44:04 +0200 blanchet speed up tautology/metaness check file | diff | annotate
Wed, 18 Jul 2012 08:44:04 +0200 blanchet more consolidation of MaSh code file | diff | annotate
Wed, 18 Jul 2012 08:44:04 +0200 blanchet drastic overhaul of MaSh data structures + fixed a few performance issues file | diff | annotate
Wed, 18 Jul 2012 08:44:04 +0200 blanchet fixed order of accessibles + other tweaks to MaSh file | diff | annotate
Wed, 18 Jul 2012 08:44:03 +0200 blanchet started implementing MaSh client-side I/O file | diff | annotate
Wed, 18 Jul 2012 08:44:03 +0200 blanchet centrally construct expensive data structures 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
Tue, 10 Jul 2012 23:36:03 +0200 blanchet MaSh evaluation driver file | diff | annotate
Tue, 10 Jul 2012 23:36:03 +0200 blanchet moved MaSh into own files file | diff | annotate
Tue, 10 Jul 2012 23:36:03 +0200 blanchet distinguish updates and queries + cleanups file | diff | annotate
Tue, 10 Jul 2012 23:36:03 +0200 blanchet better tautology elimination file | diff | annotate
Tue, 10 Jul 2012 23:36:03 +0200 blanchet generate lambdas and skolems again file | diff | annotate
Tue, 10 Jul 2012 23:36:03 +0200 blanchet generate deep terms as feature file | diff | annotate
Tue, 10 Jul 2012 23:36:03 +0200 blanchet generate theory name as a feature file | diff | annotate
Mon, 09 Jul 2012 23:58:05 +0200 blanchet compile file | diff | annotate
Mon, 09 Jul 2012 23:23:12 +0200 blanchet more precise dependencies -- eliminate tautologies file | diff | annotate
Mon, 09 Jul 2012 23:23:12 +0200 blanchet generate problem file file | diff | annotate
Mon, 09 Jul 2012 23:23:12 +0200 blanchet improve feature list generation file | diff | annotate
Mon, 09 Jul 2012 23:23:12 +0200 blanchet cleaner accessibility file file | diff | annotate
Mon, 09 Jul 2012 23:23:12 +0200 blanchet first go at generating files for MaSh (machine-learning Sledgehammer) file | diff | annotate
Tue, 26 Jun 2012 11:14:40 +0200 blanchet finished implementation of DFG type class output file | diff | annotate
Tue, 26 Jun 2012 11:14:40 +0200 blanchet more work on class support file | diff | annotate
Tue, 26 Jun 2012 11:14:40 +0200 blanchet cleanly distinguish between type declarations and symbol declarations file | diff | annotate
Tue, 26 Jun 2012 11:14:39 +0200 blanchet added type arguments to "ATerm" constructor -- but don't use them yet file | diff | annotate
Tue, 26 Jun 2012 11:14:39 +0200 blanchet started adding polymophic SPASS output file | diff | annotate
Tue, 26 Jun 2012 11:14:39 +0200 blanchet tuning file | diff | annotate
less more (0) -60 tip
isabelle