| Wed, 27 Aug 2008 11:49:14 +0200 |
wenzelm |
added General/properties.ML;
|
changeset |
files
|
| Wed, 27 Aug 2008 11:48:54 +0200 |
wenzelm |
type Properties.T;
|
changeset |
files
|
| Wed, 27 Aug 2008 11:24:35 +0200 |
haftmann |
proper error message
|
changeset |
files
|
| Wed, 27 Aug 2008 11:24:34 +0200 |
haftmann |
proper handling of type variabl names
|
changeset |
files
|
| Wed, 27 Aug 2008 11:24:32 +0200 |
haftmann |
completing arities after subclass instance
|
changeset |
files
|
| Wed, 27 Aug 2008 11:24:31 +0200 |
haftmann |
untabification
|
changeset |
files
|
| Wed, 27 Aug 2008 11:24:29 +0200 |
haftmann |
tuned code generator setup
|
changeset |
files
|
| Wed, 27 Aug 2008 04:47:30 +0200 |
urbanc |
added equivariance lemmas for ex1 and the
|
changeset |
files
|
| Wed, 27 Aug 2008 01:27:33 +0200 |
huffman |
add lemmas about Rats similar to those about Reals
|
changeset |
files
|
| Tue, 26 Aug 2008 23:49:46 +0200 |
huffman |
move real_vector class proofs into vector_space and group_hom locales
|
changeset |
files
|
| Tue, 26 Aug 2008 18:59:52 +0200 |
krauss |
added distributivity of relation composition over union [simp]
|
changeset |
files
|
| Tue, 26 Aug 2008 16:36:30 +0200 |
wenzelm |
tuned append;
|
changeset |
files
|
| Tue, 26 Aug 2008 16:36:11 +0200 |
wenzelm |
command: symbols.encode;
|
changeset |
files
|
| Tue, 26 Aug 2008 16:04:22 +0200 |
ballarin |
Reorganisation of registration code.
|
changeset |
files
|
| Tue, 26 Aug 2008 14:15:44 +0200 |
krauss |
function package: name primitive defs "f_sumC_def" instead of "f_sum_def" to avoid clashes
|
changeset |
files
|