huffman [Thu, 25 Aug 2011 15:35:54 -0700] rev 44527
remove dot_lsum and dot_rsum in favor of inner_setsum_{left,right}
huffman [Thu, 25 Aug 2011 14:26:38 -0700] rev 44526
merged
huffman [Thu, 25 Aug 2011 14:25:19 -0700] rev 44525
generalize lemma finite_imp_compact_convex_hull and related lemmas
huffman [Thu, 25 Aug 2011 13:48:11 -0700] rev 44524
generalize some lemmas
huffman [Thu, 25 Aug 2011 12:52:10 -0700] rev 44523
generalize lemma convex_cone_hull
huffman [Thu, 25 Aug 2011 12:43:55 -0700] rev 44522
rename subset_{interior,closure} to {interior,closure}_mono;
remove some legacy theorem names;
huffman [Thu, 25 Aug 2011 11:57:42 -0700] rev 44521
simplify many proofs about subspace and span;
reorder premises in rule span_induct;
huffman [Thu, 25 Aug 2011 11:56:20 -0700] rev 44520
remove duplicate simp declaration
huffman [Thu, 25 Aug 2011 09:17:02 -0700] rev 44519
simplify definition of 'interior';
add lemmas interiorI and interiorE;
change lemmas interior_unique and closure_unique to rule_format;
tidy some proofs;
huffman [Wed, 24 Aug 2011 16:08:21 -0700] rev 44518
add lemma closure_union;
simplify some proofs;
huffman [Wed, 24 Aug 2011 15:32:40 -0700] rev 44517
minimize imports
huffman [Wed, 24 Aug 2011 15:06:13 -0700] rev 44516
move everything related to 'norm' method into new theory file Norm_Arith.thy
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