| Thu, 25 Aug 2011 13:48:11 -0700 |
huffman |
generalize some lemmas
|
changeset |
files
|
| Thu, 25 Aug 2011 12:52:10 -0700 |
huffman |
generalize lemma convex_cone_hull
|
changeset |
files
|
| Thu, 25 Aug 2011 12:43:55 -0700 |
huffman |
rename subset_{interior,closure} to {interior,closure}_mono;
|
changeset |
files
|
| Thu, 25 Aug 2011 11:57:42 -0700 |
huffman |
simplify many proofs about subspace and span;
|
changeset |
files
|
| Thu, 25 Aug 2011 11:56:20 -0700 |
huffman |
remove duplicate simp declaration
|
changeset |
files
|
| Thu, 25 Aug 2011 09:17:02 -0700 |
huffman |
simplify definition of 'interior';
|
changeset |
files
|
| Wed, 24 Aug 2011 16:08:21 -0700 |
huffman |
add lemma closure_union;
|
changeset |
files
|
| Wed, 24 Aug 2011 15:32:40 -0700 |
huffman |
minimize imports
|
changeset |
files
|
| Wed, 24 Aug 2011 15:06:13 -0700 |
huffman |
move everything related to 'norm' method into new theory file Norm_Arith.thy
|
changeset |
files
|
| Wed, 24 Aug 2011 12:39:42 -0700 |
huffman |
remove unused lemmas dimensionI, dimension_eq
|
changeset |
files
|
| Wed, 24 Aug 2011 11:56:57 -0700 |
huffman |
move geometric progression lemmas from Linear_Algebra.thy to Integration.thy where they are used
|
changeset |
files
|
| Fri, 26 Aug 2011 22:53:04 +0900 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
| Fri, 26 Aug 2011 09:31:56 +0900 |
Cezary Kaliszyk |
FSet: Explicit proof without mem_def
|
changeset |
files
|
| Fri, 26 Aug 2011 14:54:41 +0200 |
nipkow |
merged
|
changeset |
files
|
| Fri, 26 Aug 2011 11:22:47 +0200 |
nipkow |
added lemma
|
changeset |
files
|
| 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
|
changeset |
files
|
| Fri, 26 Aug 2011 10:12:17 +0200 |
blanchet |
comment
|
changeset |
files
|
| 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
|
changeset |
files
|
| Fri, 26 Aug 2011 01:14:49 +0200 |
blanchet |
improve completeness of polymorphic encodings
|
changeset |
files
|
| Fri, 26 Aug 2011 00:19:25 +0200 |
blanchet |
mangle tag bound declarations properly
|
changeset |
files
|
| Fri, 26 Aug 2011 00:05:45 +0200 |
blanchet |
fixed inverted logic and improve precision when handling monotonic types in polymorphic encodings
|
changeset |
files
|
| Thu, 25 Aug 2011 23:55:21 +0200 |
blanchet |
make sure that if slicing is disabled, a non-SOS slice is chosen
|
changeset |
files
|
| Thu, 25 Aug 2011 23:54:57 +0200 |
blanchet |
honor TFF Implicit
|
changeset |
files
|
| Thu, 25 Aug 2011 23:38:09 +0200 |
blanchet |
make polymorphic encodings more complete
|
changeset |
files
|
| Thu, 25 Aug 2011 22:06:25 +0200 |
blanchet |
make default unsound mode less unsound
|
changeset |
files
|
| Thu, 25 Aug 2011 22:05:18 +0200 |
blanchet |
make TFF output less explicit where possible
|
changeset |
files
|
| Thu, 25 Aug 2011 19:09:39 +0200 |
blanchet |
use more appropriate encoding for Z3 TPTP, as confirmed by evaluation
|
changeset |
files
|
| Thu, 25 Aug 2011 19:05:40 +0200 |
blanchet |
added one more known Z3 failure
|
changeset |
files
|
| Thu, 25 Aug 2011 19:02:47 +0200 |
blanchet |
added config options to control two aspects of the translation, for evaluation purposes
|
changeset |
files
|
| Thu, 25 Aug 2011 13:55:52 +0100 |
nik |
added choice operator output for
|
changeset |
files
|
| Thu, 25 Aug 2011 14:25:07 +0200 |
blanchet |
rationalized option names -- mono becomes raw_mono and mangled becomes mono
|
changeset |
files
|
| 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
|
changeset |
files
|
| 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
|
changeset |
files
|
| Thu, 25 Aug 2011 14:25:06 +0200 |
blanchet |
fixed bang encoding detection of which types to encode
|
changeset |
files
|
| Thu, 25 Aug 2011 14:06:34 +0200 |
krauss |
lemma Compl_insert: "- insert x A = (-A) - {x}"
|
changeset |
files
|
| Thu, 25 Aug 2011 11:15:31 +0200 |
boehmes |
avoid variable clashes by properly incrementing indices
|
changeset |
files
|
| Thu, 25 Aug 2011 11:15:31 +0200 |
boehmes |
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
|
changeset |
files
|
| Thu, 25 Aug 2011 00:00:36 +0200 |
blanchet |
include chained facts for minimizer, otherwise it won't work
|
changeset |
files
|
| 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
|
changeset |
files
|
| Fri, 26 Aug 2011 22:25:41 +0200 |
wenzelm |
back to tradition Scratch.thy default -- execution wrt. perspective overcomes the main problems of 226563829580;
|
changeset |
files
|
| Fri, 26 Aug 2011 22:14:12 +0200 |
wenzelm |
tuned Session.edit_node: update_perspective based on last_exec_offset;
|
changeset |
files
|
| Fri, 26 Aug 2011 21:27:58 +0200 |
wenzelm |
tuned signature -- iterate subsumes both fold and get_first;
|
changeset |
files
|
| Fri, 26 Aug 2011 21:18:42 +0200 |
wenzelm |
further clarification of Document.updated, based on last_common and after_entry;
|
changeset |
files
|
| Fri, 26 Aug 2011 16:06:58 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Fri, 26 Aug 2011 15:56:30 +0200 |
wenzelm |
improved Document.edit: more accurate update_start and no_execs;
|
changeset |
files
|
| Fri, 26 Aug 2011 15:09:54 +0200 |
wenzelm |
refined document state assignment: observe perspective, more explicit assignment message;
|
changeset |
files
|
| Thu, 25 Aug 2011 19:12:58 +0200 |
wenzelm |
tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
|
changeset |
files
|
| Thu, 25 Aug 2011 17:38:12 +0200 |
wenzelm |
maintain last_execs assignment on Scala side;
|
changeset |
files
|
| Thu, 25 Aug 2011 16:44:06 +0200 |
wenzelm |
propagate information about last command with exec state assignment through document model;
|
changeset |
files
|
| Thu, 25 Aug 2011 13:24:41 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 25 Aug 2011 11:41:48 +0200 |
wenzelm |
slightly more abstract Command.Perspective;
|
changeset |
files
|
| Thu, 25 Aug 2011 11:27:37 +0200 |
wenzelm |
slightly more abstract Text.Perspective;
|
changeset |
files
|
| Wed, 24 Aug 2011 23:20:05 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Wed, 24 Aug 2011 23:19:40 +0200 |
wenzelm |
tuned syntax -- avoid ambiguities;
|
changeset |
files
|
| Wed, 24 Aug 2011 23:00:53 +0200 |
wenzelm |
more accurate treatment of index syntax constants, for proper entity references in concrete notation (e.g. infix "\<oplus>\<index>");
|
changeset |
files
|
| Wed, 24 Aug 2011 09:23:26 -0700 |
huffman |
delete commented-out dead code
|
changeset |
files
|
| Wed, 24 Aug 2011 09:08:07 -0700 |
huffman |
merged
|
changeset |
files
|
| Wed, 24 Aug 2011 09:08:00 -0700 |
huffman |
change some subsection headings to subsubsection
|
changeset |
files
|
| Tue, 23 Aug 2011 16:47:48 -0700 |
huffman |
remove unnecessary lemma card_ge1
|
changeset |
files
|
| Tue, 23 Aug 2011 16:17:22 -0700 |
huffman |
move connected_real_lemma to the one place it is used
|
changeset |
files
|