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/Tools/ATP/atp_proof_reconstruct.ML
Tue, 05 Aug 2014 10:59:40 +0200 blanchet rationalize Skolem names file | diff | annotate
Tue, 05 Aug 2014 10:02:35 +0200 blanchet tuned code file | diff | annotate
Tue, 05 Aug 2014 09:58:23 +0200 blanchet don't rename variables which will be renamed later anyway file | diff | annotate
Tue, 05 Aug 2014 09:55:42 +0200 blanchet normalize skolem argument variable names so that they coincide when taking the conjunction file | diff | annotate
Tue, 05 Aug 2014 09:20:00 +0200 blanchet tuning file | diff | annotate
Mon, 04 Aug 2014 16:53:09 +0200 blanchet deal with E definitions file | diff | annotate
Fri, 01 Aug 2014 23:29:50 +0200 blanchet fine-tuned Isar reconstruction, esp. boolean simplifications file | diff | annotate
Fri, 01 Aug 2014 23:29:49 +0200 blanchet centralized boolean simplification so that e.g. LEO-II benefits from it file | diff | annotate
Fri, 01 Aug 2014 20:44:29 +0200 blanchet better handling of variable names file | diff | annotate
Wed, 30 Jul 2014 23:52:56 +0200 blanchet unlift before uncombine, because the definition of a lambda-lifted symbol might have an SK combinator in it (in hybrid encodings) file | diff | annotate
Wed, 30 Jul 2014 14:03:13 +0200 fleury Whitespace and indentation correction. file | diff | annotate
Wed, 30 Jul 2014 14:03:12 +0200 fleury imported patch hilbert_choice_support file | diff | annotate
Wed, 30 Jul 2014 14:03:12 +0200 fleury imported patch satallax_proof_support_Sledgehammer file | diff | annotate
Wed, 30 Jul 2014 14:03:11 +0200 fleury removing the '= True' generated by Leo-II. file | diff | annotate
Wed, 30 Jul 2014 00:50:41 +0200 blanchet also try 'metis' with 'full_types' file | diff | annotate
Mon, 28 Jul 2014 10:57:33 +0200 blanchet correctly translate THF functions from terms to types file | diff | annotate
Thu, 24 Jul 2014 00:24:00 +0200 blanchet more robust handling of types for skolems (modeled as Frees) file | diff | annotate
Sat, 12 Jul 2014 11:31:23 +0200 blanchet don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax file | diff | annotate
Mon, 16 Jun 2014 19:42:44 +0200 blanchet integrated new Waldmeister code with 'sledgehammer' command file | diff | annotate
Mon, 16 Jun 2014 19:40:59 +0200 blanchet simplified code file | diff | annotate
Mon, 16 Jun 2014 16:21:52 +0200 fleury Moving the remote prefix deleting on Sledgehammer's side file | diff | annotate
Mon, 16 Jun 2014 16:21:39 +0200 fleury Correcting the type parser file | diff | annotate
Mon, 16 Jun 2014 16:18:34 +0200 fleury imported patch leo2_skolem_simplication file | diff | annotate
Mon, 16 Jun 2014 16:18:15 +0200 fleury add support for Isar reconstruction for thf1 ATP provers like Leo-II. file | diff | annotate
Tue, 10 Jun 2014 11:38:53 +0200 blanchet tuning file | diff | annotate
Sun, 04 May 2014 19:27:28 +0200 blanchet fixed Waldmeister endgame w.r.t. "Trueprop" file | diff | annotate
Sat, 22 Mar 2014 18:19:57 +0100 wenzelm more antiquotations; file | diff | annotate
Thu, 13 Mar 2014 14:48:20 +0100 blanchet correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs file | diff | annotate
Mon, 03 Feb 2014 15:19:07 +0100 blanchet merged 'reconstructors' and 'proof methods' file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet rationalized threading of 'metis' arguments file | diff | annotate
Thu, 30 Jan 2014 22:42:29 +0100 blanchet reverted unsound optimization file | diff | annotate
Thu, 30 Jan 2014 20:39:49 +0100 blanchet unskolemize SPASS formula to ensure that the variables are in the right order for 'metis's skolemizer file | diff | annotate
Thu, 30 Jan 2014 16:40:31 +0100 blanchet centralized & repaired handling of bound variables in intermediate data structure (viva de Bruijn) file | diff | annotate
Thu, 19 Dec 2013 17:11:54 +0100 blanchet pick up tfree/tvar type from SPASS-Pirate proof file | diff | annotate
Thu, 19 Dec 2013 16:11:20 +0100 blanchet tuning file | diff | annotate
Thu, 19 Dec 2013 15:47:17 +0100 blanchet extended ATP types with sorts file | diff | annotate
Thu, 19 Dec 2013 15:04:21 +0100 blanchet removed debugging output file | diff | annotate
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
less more (0) -60 tip
isabelle