Sat, 27 Aug 2011 13:26:06 +0200 wenzelm more precise treatment of nodes that are fully required for partially visible ones;
Sat, 27 Aug 2011 12:22:24 +0200 wenzelm de-assigned commands also count as changed;
Sat, 27 Aug 2011 11:22:21 +0200 blanchet beef up sledgehammer_tac in Mirabelle some more
Sat, 27 Aug 2011 11:22:11 +0200 blanchet merged
Fri, 26 Aug 2011 21:52:11 +0200 blanchet change default for generation of tag idempotence and tag argument equations
Fri, 26 Aug 2011 15:11:33 -0700 huffman merged
Fri, 26 Aug 2011 15:11:26 -0700 huffman NEWS entry for setsum_norm ~> norm_setsum
Fri, 26 Aug 2011 15:00:00 -0700 huffman make HOL-Probability respect set/pred distinction
Fri, 26 Aug 2011 23:14:36 +0200 wenzelm merged
Wed, 08 Sep 2010 16:10:49 -0700 huffman use rename_tac to make proof script more robust (with separate set type, 'clarify' yields different variable names)
Fri, 26 Aug 2011 10:38:29 -0700 huffman merged
Fri, 26 Aug 2011 08:56:29 -0700 huffman generalize and simplify proof of continuous_within_sequentially
Fri, 26 Aug 2011 08:12:38 -0700 huffman add lemma sequentially_imp_eventually_within;
Thu, 25 Aug 2011 19:41:38 -0700 huffman replace some continuous_on lemmas with more general versions
Thu, 25 Aug 2011 16:50:55 -0700 huffman remove legacy theorem Lim_inner
Thu, 25 Aug 2011 16:42:13 -0700 huffman arrange everything related to ordered_euclidean_space class together
Thu, 25 Aug 2011 16:06:50 -0700 huffman generalize and shorten proof of basis_orthogonal
Thu, 25 Aug 2011 15:35:54 -0700 huffman remove dot_lsum and dot_rsum in favor of inner_setsum_{left,right}
Thu, 25 Aug 2011 14:26:38 -0700 huffman merged
Thu, 25 Aug 2011 14:25:19 -0700 huffman generalize lemma finite_imp_compact_convex_hull and related lemmas
Thu, 25 Aug 2011 13:48:11 -0700 huffman generalize some lemmas
Thu, 25 Aug 2011 12:52:10 -0700 huffman generalize lemma convex_cone_hull
Thu, 25 Aug 2011 12:43:55 -0700 huffman rename subset_{interior,closure} to {interior,closure}_mono;
Thu, 25 Aug 2011 11:57:42 -0700 huffman simplify many proofs about subspace and span;
Thu, 25 Aug 2011 11:56:20 -0700 huffman remove duplicate simp declaration
Thu, 25 Aug 2011 09:17:02 -0700 huffman simplify definition of 'interior';
Wed, 24 Aug 2011 16:08:21 -0700 huffman add lemma closure_union;
Wed, 24 Aug 2011 15:32:40 -0700 huffman minimize imports
Wed, 24 Aug 2011 15:06:13 -0700 huffman move everything related to 'norm' method into new theory file Norm_Arith.thy
Wed, 24 Aug 2011 12:39:42 -0700 huffman remove unused lemmas dimensionI, dimension_eq
Wed, 24 Aug 2011 11:56:57 -0700 huffman move geometric progression lemmas from Linear_Algebra.thy to Integration.thy where they are used
Fri, 26 Aug 2011 22:53:04 +0900 Cezary Kaliszyk merge
Fri, 26 Aug 2011 09:31:56 +0900 Cezary Kaliszyk FSet: Explicit proof without mem_def
Fri, 26 Aug 2011 14:54:41 +0200 nipkow merged
Fri, 26 Aug 2011 11:22:47 +0200 nipkow added lemma
Fri, 26 Aug 2011 10:25:13 +0200 blanchet 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
Fri, 26 Aug 2011 10:12:17 +0200 blanchet comment
Fri, 26 Aug 2011 01:18:48 +0200 blanchet disable TFF for Vampire 1.8 until they've fixed the soundness issues and it's back on SystemOnTPTP
Fri, 26 Aug 2011 01:14:49 +0200 blanchet improve completeness of polymorphic encodings
Fri, 26 Aug 2011 00:19:25 +0200 blanchet mangle tag bound declarations properly
Fri, 26 Aug 2011 00:05:45 +0200 blanchet fixed inverted logic and improve precision when handling monotonic types in polymorphic encodings
Thu, 25 Aug 2011 23:55:21 +0200 blanchet make sure that if slicing is disabled, a non-SOS slice is chosen
Thu, 25 Aug 2011 23:54:57 +0200 blanchet honor TFF Implicit
Thu, 25 Aug 2011 23:38:09 +0200 blanchet make polymorphic encodings more complete
Thu, 25 Aug 2011 22:06:25 +0200 blanchet make default unsound mode less unsound
Thu, 25 Aug 2011 22:05:18 +0200 blanchet make TFF output less explicit where possible
Thu, 25 Aug 2011 19:09:39 +0200 blanchet use more appropriate encoding for Z3 TPTP, as confirmed by evaluation
Thu, 25 Aug 2011 19:05:40 +0200 blanchet added one more known Z3 failure
Thu, 25 Aug 2011 19:02:47 +0200 blanchet added config options to control two aspects of the translation, for evaluation purposes
Thu, 25 Aug 2011 13:55:52 +0100 nik added choice operator output for
Thu, 25 Aug 2011 14:25:07 +0200 blanchet rationalized option names -- mono becomes raw_mono and mangled becomes mono
Thu, 25 Aug 2011 14:25:07 +0200 blanchet handle nonmangled monomorphich the same way as mangled monomorphic when it comes to helper -- otherwise we can end up generating too tight type guards
Thu, 25 Aug 2011 14:25:07 +0200 blanchet avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
Thu, 25 Aug 2011 14:25:06 +0200 blanchet fixed bang encoding detection of which types to encode
Thu, 25 Aug 2011 14:06:34 +0200 krauss lemma Compl_insert: "- insert x A = (-A) - {x}"
Thu, 25 Aug 2011 11:15:31 +0200 boehmes avoid variable clashes by properly incrementing indices
Thu, 25 Aug 2011 11:15:31 +0200 boehmes improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
Thu, 25 Aug 2011 00:00:36 +0200 blanchet include chained facts for minimizer, otherwise it won't work
Wed, 24 Aug 2011 22:12:30 +0200 blanchet 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
Fri, 26 Aug 2011 22:25:41 +0200 wenzelm back to tradition Scratch.thy default -- execution wrt. perspective overcomes the main problems of 226563829580;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip