| 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
|