| Sun, 28 Aug 2011 08:12:54 +0200 |
haftmann |
corrected slip
|
changeset |
files
|
| Sat, 27 Aug 2011 19:52:58 +0200 |
haftmann |
Cset, Dlist_Cset, List_Cset: restructured
|
changeset |
files
|
| Sat, 27 Aug 2011 09:44:45 +0200 |
haftmann |
Cset, Dlist_Cset, List_Cset: restructured
|
changeset |
files
|
| Sat, 27 Aug 2011 09:02:25 +0200 |
haftmann |
adapted to changes in Cset.thy
|
changeset |
files
|
| Fri, 26 Aug 2011 23:02:00 +0200 |
haftmann |
adapted to changes in Cset.thy
|
changeset |
files
|
| Fri, 26 Aug 2011 21:11:23 +0200 |
haftmann |
separating predicates and sets syntactically
|
changeset |
files
|
| Fri, 26 Aug 2011 18:24:22 +0200 |
haftmann |
merged
|
changeset |
files
|
| Fri, 26 Aug 2011 18:23:33 +0200 |
haftmann |
avoid intermixing set and predicates; dropped lemmas mem_rsp and mem_prs (now in Quotient_Set.thy)
|
changeset |
files
|
| Thu, 25 Aug 2011 23:32:12 +0200 |
haftmann |
updated generated files
|
changeset |
files
|
| Thu, 25 Aug 2011 23:20:44 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 25 Aug 2011 23:20:34 +0200 |
haftmann |
updated generated files
|
changeset |
files
|
| Sat, 27 Aug 2011 17:26:14 +0200 |
wenzelm |
explicit markup for legacy warnings;
|
changeset |
files
|
| Sat, 27 Aug 2011 16:22:59 +0200 |
wenzelm |
updated generated files;
|
changeset |
files
|
| Sat, 27 Aug 2011 16:11:24 +0200 |
wenzelm |
less aggressive warning icon;
|
changeset |
files
|
| Sat, 27 Aug 2011 16:01:24 +0200 |
wenzelm |
tuned colors;
|
changeset |
files
|
| Sat, 27 Aug 2011 15:53:18 +0200 |
wenzelm |
transparent foreground color for quoted entities;
|
changeset |
files
|
| Sat, 27 Aug 2011 13:26:06 +0200 |
wenzelm |
more precise treatment of nodes that are fully required for partially visible ones;
|
changeset |
files
|
| Sat, 27 Aug 2011 12:22:24 +0200 |
wenzelm |
de-assigned commands also count as changed;
|
changeset |
files
|
| Sat, 27 Aug 2011 11:22:21 +0200 |
blanchet |
beef up sledgehammer_tac in Mirabelle some more
|
changeset |
files
|
| Sat, 27 Aug 2011 11:22:11 +0200 |
blanchet |
merged
|
changeset |
files
|
| Fri, 26 Aug 2011 21:52:11 +0200 |
blanchet |
change default for generation of tag idempotence and tag argument equations
|
changeset |
files
|
| Fri, 26 Aug 2011 15:11:33 -0700 |
huffman |
merged
|
changeset |
files
|
| Fri, 26 Aug 2011 15:11:26 -0700 |
huffman |
NEWS entry for setsum_norm ~> norm_setsum
|
changeset |
files
|
| Fri, 26 Aug 2011 15:00:00 -0700 |
huffman |
make HOL-Probability respect set/pred distinction
|
changeset |
files
|
| Fri, 26 Aug 2011 23:14:36 +0200 |
wenzelm |
merged
|
changeset |
files
|
| 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)
|
changeset |
files
|
| Fri, 26 Aug 2011 10:38:29 -0700 |
huffman |
merged
|
changeset |
files
|
| Fri, 26 Aug 2011 08:56:29 -0700 |
huffman |
generalize and simplify proof of continuous_within_sequentially
|
changeset |
files
|
| Fri, 26 Aug 2011 08:12:38 -0700 |
huffman |
add lemma sequentially_imp_eventually_within;
|
changeset |
files
|
| Thu, 25 Aug 2011 19:41:38 -0700 |
huffman |
replace some continuous_on lemmas with more general versions
|
changeset |
files
|
| Thu, 25 Aug 2011 16:50:55 -0700 |
huffman |
remove legacy theorem Lim_inner
|
changeset |
files
|
| Thu, 25 Aug 2011 16:42:13 -0700 |
huffman |
arrange everything related to ordered_euclidean_space class together
|
changeset |
files
|
| Thu, 25 Aug 2011 16:06:50 -0700 |
huffman |
generalize and shorten proof of basis_orthogonal
|
changeset |
files
|
| Thu, 25 Aug 2011 15:35:54 -0700 |
huffman |
remove dot_lsum and dot_rsum in favor of inner_setsum_{left,right}
|
changeset |
files
|
| Thu, 25 Aug 2011 14:26:38 -0700 |
huffman |
merged
|
changeset |
files
|
| Thu, 25 Aug 2011 14:25:19 -0700 |
huffman |
generalize lemma finite_imp_compact_convex_hull and related lemmas
|
changeset |
files
|
| 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
|