| Mon, 08 Jun 2009 07:22:35 -0700 |
huffman |
merged
|
changeset |
files
|
| Sun, 07 Jun 2009 20:57:52 -0700 |
huffman |
merged
|
changeset |
files
|
| Mon, 08 Jun 2009 09:58:41 +0200 |
nipkow |
new lemma
|
changeset |
files
|
| Mon, 08 Jun 2009 09:23:04 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 08 Jun 2009 09:03:00 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 08 Jun 2009 09:02:51 +0200 |
haftmann |
proper deresolving of class relations and class parameters in SML
|
changeset |
files
|
| Mon, 08 Jun 2009 08:52:18 +0200 |
nipkow |
New lemma
|
changeset |
files
|
| Mon, 08 Jun 2009 00:26:57 +0200 |
wenzelm |
eliminated hardwired Cygwin setup;
|
changeset |
files
|
| Mon, 08 Jun 2009 00:20:43 +0200 |
wenzelm |
Accessing the Cygwin installation.
|
changeset |
files
|
| Sun, 07 Jun 2009 20:15:29 +0200 |
wenzelm |
static IsabelleSystem.charset;
|
changeset |
files
|
| Sun, 07 Jun 2009 19:07:05 +0200 |
wenzelm |
isabelle getenv: option -d;
|
changeset |
files
|
| Sat, 06 Jun 2009 23:43:07 +0200 |
wenzelm |
no parallel make jobs on macbroy23, which is the machine where SML/XL is tested -- attempt to consume less resources;
|
changeset |
files
|
| Sat, 06 Jun 2009 21:57:50 +0200 |
wenzelm |
updated version;
|
changeset |
files
|
| Sun, 07 Jun 2009 20:57:24 -0700 |
huffman |
fix type of open
|
changeset |
files
|
| Sun, 07 Jun 2009 19:38:32 -0700 |
huffman |
new setL2 lemmas; instance ^ :: (topological_space, finite) topological_space
|
changeset |
files
|
| Sun, 07 Jun 2009 17:59:54 -0700 |
huffman |
replace 'topo' with 'open'; add extra type constraint for 'open'
|
changeset |
files
|
| Sun, 07 Jun 2009 15:18:52 -0700 |
huffman |
generalize tendsto lemmas for products
|
changeset |
files
|
| Sun, 07 Jun 2009 12:00:03 -0700 |
huffman |
move definitions of open, closed to RealVector.thy
|
changeset |
files
|
| Sat, 06 Jun 2009 10:28:34 -0700 |
huffman |
lemmas islimptI, islimptE; generalize open_inter_closure_subset
|
changeset |
files
|
| Sat, 06 Jun 2009 09:11:12 -0700 |
huffman |
generalize tendsto to class topological_space
|
changeset |
files
|
| Fri, 05 Jun 2009 15:59:20 -0700 |
huffman |
put syntax for tendsto in Limits.thy; rename variables
|
changeset |
files
|
| Mon, 08 Jun 2009 09:22:47 +0200 |
haftmann |
constant "chars" of all characters
|
changeset |
files
|
| Mon, 08 Jun 2009 08:38:53 +0200 |
haftmann |
added infrastructure for definitorial construction of generators for datatypes
|
changeset |
files
|
| Mon, 08 Jun 2009 08:38:52 +0200 |
haftmann |
constant "chars" of all characters
|
changeset |
files
|
| Mon, 08 Jun 2009 08:38:51 +0200 |
haftmann |
added generator for char and trivial generator for String.literal
|
changeset |
files
|
| Mon, 08 Jun 2009 08:38:50 +0200 |
haftmann |
using constant "chars"
|
changeset |
files
|
| Mon, 08 Jun 2009 08:38:49 +0200 |
haftmann |
method linarith
|
changeset |
files
|
| Sat, 06 Jun 2009 21:47:02 +0200 |
wenzelm |
reraise exceptions to preserve position information;
|
changeset |
files
|
| Sat, 06 Jun 2009 21:46:36 +0200 |
wenzelm |
ML_Compiler.exn_message;
|
changeset |
files
|
| Sat, 06 Jun 2009 21:11:23 +0200 |
wenzelm |
ML_Compiler.exn_message;
|
changeset |
files
|