| Sat, 10 Sep 2011 23:28:58 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 10 Sep 2011 22:43:17 +0200 |
krauss |
mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
|
changeset |
files
|
| Sat, 10 Sep 2011 23:27:32 +0200 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Sat, 10 Sep 2011 22:11:55 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Sat, 10 Sep 2011 21:47:55 +0200 |
wenzelm |
speed up slow proof;
|
changeset |
files
|
| Sat, 10 Sep 2011 20:41:27 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 10 Sep 2011 19:44:41 +0200 |
haftmann |
more modularization
|
changeset |
files
|
| Sat, 10 Sep 2011 20:39:13 +0200 |
wenzelm |
stronger colors (as background);
|
changeset |
files
|
| Sat, 10 Sep 2011 20:22:22 +0200 |
wenzelm |
some color scheme for theory status;
|
changeset |
files
|
| Sat, 10 Sep 2011 16:30:08 +0200 |
wenzelm |
some keyboard shortcuts for important actions;
|
changeset |
files
|
| Sat, 10 Sep 2011 14:48:06 +0200 |
wenzelm |
explicit jEdit actions -- to enable key mappings, for example;
|
changeset |
files
|
| Sat, 10 Sep 2011 14:28:07 +0200 |
wenzelm |
more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;
|
changeset |
files
|
| Sat, 10 Sep 2011 13:43:09 +0200 |
wenzelm |
tuned usage;
|
changeset |
files
|
| Sat, 10 Sep 2011 13:41:03 +0200 |
wenzelm |
simplified default Isabelle application wrapper (NB: build process is already part of isabelle jedit tool);
|
changeset |
files
|
| Sat, 10 Sep 2011 10:29:24 +0200 |
haftmann |
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
|
changeset |
files
|
| Sat, 10 Sep 2011 00:44:25 +0200 |
blanchet |
fixed definition of type intersection (soundness bug)
|
changeset |
files
|
| Sat, 10 Sep 2011 00:44:25 +0200 |
blanchet |
continue with minimization in debug mode in spite of unsoundness
|
changeset |
files
|
| Fri, 09 Sep 2011 09:31:04 -0700 |
huffman |
generalize lemma of_nat_number_of_eq to class number_semiring
|
changeset |
files
|
| Fri, 09 Sep 2011 15:14:59 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Fri, 09 Sep 2011 14:43:50 +0200 |
bulwahn |
stating more explicitly our expectation that these two terms have the same term structure
|
changeset |
files
|
| Fri, 09 Sep 2011 12:33:09 +0200 |
bulwahn |
revisiting type annotations for Haskell: necessary type annotations are not inferred on the provided theorems but using the arguments and right hand sides, as these might differ in the case of constants with abstract code types
|
changeset |
files
|
| Fri, 09 Sep 2011 14:30:57 +0200 |
blanchet |
made SML/NJ happy
|
changeset |
files
|
| Thu, 08 Sep 2011 12:23:11 +0200 |
noschinl |
call ghc with -XEmptyDataDecls
|
changeset |
files
|
| Fri, 09 Sep 2011 06:47:14 +0200 |
nipkow |
merged
|
changeset |
files
|
| Fri, 09 Sep 2011 06:45:39 +0200 |
nipkow |
tuned headers
|
changeset |
files
|
| Thu, 08 Sep 2011 19:35:23 -0700 |
huffman |
Library/Saturated.thy: number_semiring class instance
|
changeset |
files
|
| Thu, 08 Sep 2011 18:47:23 -0700 |
huffman |
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
|
changeset |
files
|
| Thu, 08 Sep 2011 18:13:48 -0700 |
huffman |
merged
|
changeset |
files
|
| Thu, 08 Sep 2011 10:07:53 -0700 |
huffman |
remove unnecessary intermediate lemmas
|
changeset |
files
|
| Fri, 09 Sep 2011 00:22:18 +0200 |
krauss |
added syntactic classes for "inf" and "sup"
|
changeset |
files
|
| Thu, 08 Sep 2011 08:41:28 -0700 |
huffman |
prove existence, uniqueness, and other properties of complex arg function
|
changeset |
files
|
| Thu, 08 Sep 2011 07:27:57 -0700 |
huffman |
tuned
|
changeset |
files
|
| Thu, 08 Sep 2011 07:16:47 -0700 |
huffman |
remove obsolete intermediate lemma complex_inverse_complex_split
|
changeset |
files
|
| Thu, 08 Sep 2011 07:06:59 -0700 |
huffman |
tuned
|
changeset |
files
|
| Thu, 08 Sep 2011 11:31:53 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 08 Sep 2011 11:31:23 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 08 Sep 2011 00:35:22 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 07 Sep 2011 08:13:38 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 06 Sep 2011 22:37:32 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 06 Sep 2011 22:04:14 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 06 Sep 2011 07:23:45 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 05 Sep 2011 22:02:32 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Mon, 05 Sep 2011 19:18:38 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 05 Sep 2011 07:49:31 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Sun, 04 Sep 2011 09:28:15 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 08 Sep 2011 09:25:55 +0200 |
blanchet |
fixed computation of "in_conj" for polymorphic encodings
|
changeset |
files
|
| Wed, 07 Sep 2011 22:44:26 -0700 |
huffman |
add some new lemmas about cis and rcis;
|
changeset |
files
|
| Wed, 07 Sep 2011 20:44:39 -0700 |
huffman |
Complex.thy: move theorems into appropriate subsections
|
changeset |
files
|
| Wed, 07 Sep 2011 19:24:28 -0700 |
huffman |
merged
|
changeset |
files
|
| Wed, 07 Sep 2011 17:41:29 -0700 |
huffman |
remove redundant lemma complex_of_real_minus_one
|
changeset |
files
|
| Wed, 07 Sep 2011 18:47:55 -0700 |
huffman |
simplify proof of lemma DeMoivre, removing unnecessary intermediate lemma
|
changeset |
files
|
| Wed, 07 Sep 2011 10:04:07 -0700 |
huffman |
removed unused lemma sin_cos_squared_add2_mult
|
changeset |
files
|
| Wed, 07 Sep 2011 09:45:39 -0700 |
huffman |
remove duplicate lemma real_of_int_real_of_nat in favor of real_of_int_of_nat_eq
|
changeset |
files
|
| Wed, 07 Sep 2011 09:02:58 -0700 |
huffman |
avoid using legacy theorem names
|
changeset |
files
|
| Thu, 08 Sep 2011 00:23:23 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 07 Sep 2011 23:55:40 +0200 |
haftmann |
theory of saturated naturals contributed by Peter Gammie
|
changeset |
files
|
| Wed, 07 Sep 2011 23:38:52 +0200 |
haftmann |
theory of saturated naturals contributed by Peter Gammie
|
changeset |
files
|
| Wed, 07 Sep 2011 23:07:16 +0200 |
haftmann |
lemmas about +, *, min, max on nat
|
changeset |
files
|
| Wed, 07 Sep 2011 21:31:21 +0200 |
blanchet |
update Sledgehammer docs
|
changeset |
files
|
| Wed, 07 Sep 2011 21:31:21 +0200 |
blanchet |
added new tagged encodings to Metis tests
|
changeset |
files
|