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/ATP/atp_proof_reconstruct.ML
Thu, 19 Dec 2013 14:57:21 +0100 blanchet honor SPASS-Pirate type arguments file | diff | annotate
Wed, 18 Dec 2013 22:55:20 +0100 blanchet parse SPASS-Pirate types file | diff | annotate
Wed, 18 Dec 2013 16:50:14 +0100 blanchet tuning file | diff | annotate
Tue, 17 Dec 2013 14:15:23 +0100 blanchet tuning 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
Tue, 17 Dec 2013 09:42:38 +0100 blanchet made SML/NJ happier file | diff | annotate
Mon, 16 Dec 2013 23:05:16 +0100 blanchet handle Skolems gracefully for SPASS as well file | diff | annotate
Mon, 16 Dec 2013 20:24:13 +0100 blanchet reverse Skolem function arguments file | diff | annotate
Mon, 16 Dec 2013 17:18:52 +0100 blanchet fixed confusion between 'prop' and 'bool' introduced in 4960647932ec file | diff | annotate
Sun, 15 Dec 2013 19:01:06 +0100 blanchet use 'prop' rather than 'bool' systematically in Isar reconstruction code file | diff | annotate
Sun, 15 Dec 2013 18:54:26 +0100 blanchet tuning file | diff | annotate
Tue, 19 Nov 2013 22:20:01 +0100 blanchet whitespace tuning file | diff | annotate
Tue, 19 Nov 2013 19:42:30 +0100 blanchet tuning file | diff | annotate
Tue, 19 Nov 2013 19:36:24 +0100 blanchet more refactoring to accommodate SMT proofs file | diff | annotate
Tue, 19 Nov 2013 18:11:52 +0100 blanchet simplified old code file | diff | annotate
Tue, 19 Nov 2013 17:37:35 +0100 blanchet refactoring file | diff | annotate
Tue, 19 Nov 2013 17:12:58 +0100 blanchet refactoring file | diff | annotate
Thu, 12 Sep 2013 22:10:57 +0200 blanchet prefixed types and some functions with "atp_" for disambiguation file | diff | annotate
Mon, 29 Jul 2013 18:06:39 +0200 blanchet avoid duplicating Var when the types do not quite fit -- since this step occurs before type inference file | diff | annotate
Fri, 24 May 2013 16:43:37 +0200 blanchet improved handling of free variables' types in Isar proofs file | diff | annotate
Thu, 16 May 2013 14:58:30 +0200 blanchet correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer file | diff | annotate
Thu, 16 May 2013 13:34:13 +0200 blanchet tuning -- renamed '_from_' to '_of_' in Sledgehammer file | diff | annotate
Mon, 06 May 2013 11:03:08 +0200 smolkas handle dummy atp terms file | diff | annotate
Wed, 20 Feb 2013 08:44:24 +0100 blanchet slacker comparison for Skolems, to avoid trivial equations file | diff | annotate
Thu, 03 Jan 2013 17:10:12 +0100 blanchet rename variable in binder, not just in body file | diff | annotate
Thu, 03 Jan 2013 15:13:11 +0100 blanchet swap Vampire's Skolem arguments to bring them in line with what E and metis's new skolemizer do (helps Isar proof reconstruction in some cases) file | diff | annotate
Thu, 03 Jan 2013 00:02:15 +0100 blanchet tuned comment file | diff | annotate
Wed, 02 Jan 2013 19:59:06 +0100 blanchet generate "obtain" steps corresponding to skolemization inferences file | diff | annotate
Wed, 02 Jan 2013 13:14:47 +0100 blanchet properly take the existential closure of skolems file | diff | annotate
Wed, 31 Oct 2012 11:23:21 +0100 blanchet use metaquantification when possible in Isar proofs file | diff | annotate
Thu, 18 Oct 2012 13:19:44 +0200 blanchet refactor code file | diff | annotate
Tue, 16 Oct 2012 18:50:53 +0200 blanchet added proof minimization code from Steffen Smolka file | diff | annotate
Tue, 09 Oct 2012 00:40:33 +0200 blanchet added type annotations to generated Isar proofs -- code by Steffen Smolka file | diff | annotate
Tue, 14 Aug 2012 14:07:53 +0200 blanchet warn users about unused "using" facts file | diff | annotate
Fri, 27 Jul 2012 08:52:40 +0200 blanchet extract Z3 unsat cores (for "z3_tptp") 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
Tue, 26 Jun 2012 11:14:40 +0200 blanchet added sorts to datastructure 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
Wed, 06 Jun 2012 10:35:05 +0200 blanchet avoid dumping definitions several times in LEO-II proofs file | diff | annotate
Wed, 23 May 2012 21:19:48 +0200 blanchet improved LEO-II definition handling -- still hoping for a fix directly in LEO-II file | diff | annotate
Wed, 23 May 2012 21:19:48 +0200 blanchet augment Satallax unsat cores with all definitions file | diff | annotate
Mon, 21 May 2012 11:31:52 +0200 blanchet include "ext" in all Satallax proofs file | diff | annotate
Tue, 15 May 2012 13:06:15 +0200 blanchet repair the Waldmeister endgame only for Waldmeister proofs file | diff | annotate
Mon, 14 May 2012 15:54:26 +0200 blanchet ensure the "show" equation is not reoriented by Waldmeister file | diff | annotate
Mon, 14 May 2012 15:54:26 +0200 blanchet ensure consistent naming of Waldmeister proof steps, so that they are not cleaned away by "clean_up_atp_proof_dependencies" file | diff | annotate
Mon, 14 May 2012 15:54:26 +0200 blanchet graceful handling of Waldmeister endgame file | diff | annotate
Thu, 26 Apr 2012 00:33:23 +0200 blanchet tuning file | diff | annotate
Tue, 27 Mar 2012 16:59:13 +0300 blanchet print a hint file | diff | annotate
Tue, 13 Mar 2012 16:40:06 +0100 wenzelm prefer abs_def over def_raw; file | diff | annotate
Mon, 27 Feb 2012 16:56:25 +0100 wenzelm more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile); file | diff | annotate
Mon, 06 Feb 2012 23:01:01 +0100 blanchet renamed type encoding file | diff | annotate
Sun, 05 Feb 2012 12:27:10 +0100 blanchet cleaned up new SPASS parsing file | diff | annotate
Mon, 30 Jan 2012 17:15:59 +0100 blanchet avoid unsupported case in Metis file | diff | annotate
Mon, 30 Jan 2012 17:15:59 +0100 blanchet rename lambda translation schemes file | diff | annotate
Fri, 27 Jan 2012 10:19:55 +0100 blanchet made SML/NJ happy file | diff | annotate
Thu, 26 Jan 2012 20:49:54 +0100 blanchet separate orthogonal components file | diff | annotate
Mon, 23 Jan 2012 17:40:32 +0100 blanchet renamed two files to make room for a new file file | diff | annotate | base
less more (0) tip
isabelle