| Sat, 19 May 2007 13:41:13 +0200 |
nipkow |
added code generation based on Isabelle's rat type.
|
changeset |
files
|
| Sat, 19 May 2007 13:40:33 +0200 |
nipkow |
Disabled Stefancs code generator - already enabled in RealDef.
|
changeset |
files
|
| Sat, 19 May 2007 11:33:57 +0200 |
haftmann |
constant op @ now named append
|
changeset |
files
|
| Sat, 19 May 2007 11:33:34 +0200 |
haftmann |
fixed comment
|
changeset |
files
|
| Sat, 19 May 2007 11:33:33 +0200 |
haftmann |
dropped legacy
|
changeset |
files
|
| Sat, 19 May 2007 11:33:32 +0200 |
haftmann |
improved eta expansion
|
changeset |
files
|
| Sat, 19 May 2007 11:33:31 +0200 |
haftmann |
dropped nonsense comment
|
changeset |
files
|
| Sat, 19 May 2007 11:33:30 +0200 |
haftmann |
fixed text
|
changeset |
files
|
| Sat, 19 May 2007 11:33:28 +0200 |
haftmann |
eliminated name clash with List.append
|
changeset |
files
|
| Sat, 19 May 2007 11:33:26 +0200 |
haftmann |
added qualification for ambiguous definition names
|
changeset |
files
|
| Sat, 19 May 2007 11:33:25 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Sat, 19 May 2007 11:33:24 +0200 |
haftmann |
typ_of instance for int
|
changeset |
files
|
| Sat, 19 May 2007 11:33:23 +0200 |
haftmann |
hide locale predicate "field" from HOL library
|
changeset |
files
|
| Sat, 19 May 2007 11:33:22 +0200 |
haftmann |
no special treatment in naming of locale predicates stemming form classes
|
changeset |
files
|
| Sat, 19 May 2007 11:33:21 +0200 |
haftmann |
uniform module names for code generation
|
changeset |
files
|