| Fri, 20 Feb 2009 14:49:24 +0100 |
haftmann |
reverted to old wellsorting algorithm
|
changeset |
files
|
| Fri, 20 Feb 2009 14:49:23 +0100 |
haftmann |
fixed spurious proof failure
|
changeset |
files
|
| Fri, 20 Feb 2009 14:49:23 +0100 |
haftmann |
consider changes variable names in theorem le_imp_power_dvd
|
changeset |
files
|
| Fri, 20 Feb 2009 10:14:32 +0100 |
haftmann |
tuned and incremental version of wellsorting algorithm
|
changeset |
files
|
| Fri, 20 Feb 2009 10:14:32 +0100 |
haftmann |
ignore sorts in bare types
|
changeset |
files
|
| Fri, 20 Feb 2009 10:14:32 +0100 |
haftmann |
defensive implementation of pretty serialisation of lists and characters
|
changeset |
files
|
| Fri, 20 Feb 2009 10:14:31 +0100 |
haftmann |
dropped Id
|
changeset |
files
|
| Fri, 20 Feb 2009 10:14:31 +0100 |
haftmann |
experimental inclusion of new wellsorting algorithm for code equations
|
changeset |
files
|
| Fri, 20 Feb 2009 13:14:57 +0000 |
chaieb |
merged
|
changeset |
files
|
| Tue, 17 Feb 2009 21:51:48 +0000 |
chaieb |
merged
|
changeset |
files
|
| Tue, 17 Feb 2009 20:42:19 +0000 |
chaieb |
merged
|
changeset |
files
|
| Tue, 17 Feb 2009 20:41:36 +0000 |
chaieb |
fixed selection of premises
|
changeset |
files
|
| Thu, 19 Feb 2009 23:18:28 -0800 |
huffman |
cleaned up
|
changeset |
files
|
| Thu, 19 Feb 2009 18:16:19 -0800 |
huffman |
declare of_int_number_of_eq [simp]
|
changeset |
files
|
| Thu, 19 Feb 2009 17:13:35 -0800 |
huffman |
fix case_names
|
changeset |
files
|
| Thu, 19 Feb 2009 17:11:12 -0800 |
huffman |
nicer induction/cases rules for numeral types
|
changeset |
files
|