src/HOL/Tools/ATP/atp_proof_reconstruct.ML
Sat, 09 Aug 2014 21:03:42 +0200 wenzelm tuned;
Tue, 05 Aug 2014 10:59:40 +0200 blanchet rationalize Skolem names
Tue, 05 Aug 2014 10:02:35 +0200 blanchet tuned code
Tue, 05 Aug 2014 09:58:23 +0200 blanchet don't rename variables which will be renamed later anyway
Tue, 05 Aug 2014 09:55:42 +0200 blanchet normalize skolem argument variable names so that they coincide when taking the conjunction
Tue, 05 Aug 2014 09:20:00 +0200 blanchet tuning
Mon, 04 Aug 2014 16:53:09 +0200 blanchet deal with E definitions
Fri, 01 Aug 2014 23:29:50 +0200 blanchet fine-tuned Isar reconstruction, esp. boolean simplifications
Fri, 01 Aug 2014 23:29:49 +0200 blanchet centralized boolean simplification so that e.g. LEO-II benefits from it
Fri, 01 Aug 2014 20:44:29 +0200 blanchet better handling of variable names
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)
Wed, 30 Jul 2014 14:03:13 +0200 fleury Whitespace and indentation correction.
Wed, 30 Jul 2014 14:03:12 +0200 fleury imported patch hilbert_choice_support
Wed, 30 Jul 2014 14:03:12 +0200 fleury imported patch satallax_proof_support_Sledgehammer
Wed, 30 Jul 2014 14:03:11 +0200 fleury removing the '= True' generated by Leo-II.
less more (0) -15 tip