huffman [Wed, 24 Aug 2011 12:39:42 -0700] rev 44515
remove unused lemmas dimensionI, dimension_eq
huffman [Wed, 24 Aug 2011 11:56:57 -0700] rev 44514
move geometric progression lemmas from Linear_Algebra.thy to Integration.thy where they are used
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 26 Aug 2011 22:53:04 +0900] rev 44513
merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 26 Aug 2011 09:31:56 +0900] rev 44512
FSet: Explicit proof without mem_def
nipkow [Fri, 26 Aug 2011 14:54:41 +0200] rev 44511
merged
nipkow [Fri, 26 Aug 2011 11:22:47 +0200] rev 44510
added lemma
blanchet [Fri, 26 Aug 2011 10:25:13 +0200] rev 44509
added a component in generated file names reflecting whether the minimizer is used -- needed for evaluation to keep these files separated from the main problem files
blanchet [Fri, 26 Aug 2011 10:12:17 +0200] rev 44508
comment
blanchet [Fri, 26 Aug 2011 01:18:48 +0200] rev 44507
disable TFF for Vampire 1.8 until they've fixed the soundness issues and it's back on SystemOnTPTP
blanchet [Fri, 26 Aug 2011 01:14:49 +0200] rev 44506
improve completeness of polymorphic encodings
blanchet [Fri, 26 Aug 2011 00:19:25 +0200] rev 44505
mangle tag bound declarations properly
blanchet [Fri, 26 Aug 2011 00:05:45 +0200] rev 44504
fixed inverted logic and improve precision when handling monotonic types in polymorphic encodings
blanchet [Thu, 25 Aug 2011 23:55:21 +0200] rev 44503
make sure that if slicing is disabled, a non-SOS slice is chosen
blanchet [Thu, 25 Aug 2011 23:54:57 +0200] rev 44502
honor TFF Implicit
blanchet [Thu, 25 Aug 2011 23:38:09 +0200] rev 44501
make polymorphic encodings more complete
blanchet [Thu, 25 Aug 2011 22:06:25 +0200] rev 44500
make default unsound mode less unsound
blanchet [Thu, 25 Aug 2011 22:05:18 +0200] rev 44499
make TFF output less explicit where possible
blanchet [Thu, 25 Aug 2011 19:09:39 +0200] rev 44498
use more appropriate encoding for Z3 TPTP, as confirmed by evaluation
blanchet [Thu, 25 Aug 2011 19:05:40 +0200] rev 44497
added one more known Z3 failure
blanchet [Thu, 25 Aug 2011 19:02:47 +0200] rev 44496
added config options to control two aspects of the translation, for evaluation purposes
nik [Thu, 25 Aug 2011 13:55:52 +0100] rev 44495
added choice operator output for
Satallax
blanchet [Thu, 25 Aug 2011 14:25:07 +0200] rev 44494
rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet [Thu, 25 Aug 2011 14:25:07 +0200] rev 44493
handle nonmangled monomorphich the same way as mangled monomorphic when it comes to helper -- otherwise we can end up generating too tight type guards
blanchet [Thu, 25 Aug 2011 14:25:07 +0200] rev 44492
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet [Thu, 25 Aug 2011 14:25:06 +0200] rev 44491
fixed bang encoding detection of which types to encode
krauss [Thu, 25 Aug 2011 14:06:34 +0200] rev 44490
lemma Compl_insert: "- insert x A = (-A) - {x}"
boehmes [Thu, 25 Aug 2011 11:15:31 +0200] rev 44489
avoid variable clashes by properly incrementing indices
boehmes [Thu, 25 Aug 2011 11:15:31 +0200] rev 44488
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
blanchet [Thu, 25 Aug 2011 00:00:36 +0200] rev 44487
include chained facts for minimizer, otherwise it won't work
blanchet [Wed, 24 Aug 2011 22:12:30 +0200] rev 44486
remove Vampire imconplete proof detection -- the bug it was trying to work around has been fixed in version 1.8, and the check is too sensitive anyway
wenzelm [Fri, 26 Aug 2011 22:25:41 +0200] rev 44485
back to tradition Scratch.thy default -- execution wrt. perspective overcomes the main problems of 226563829580;
wenzelm [Fri, 26 Aug 2011 22:14:12 +0200] rev 44484
tuned Session.edit_node: update_perspective based on last_exec_offset;