| Fri, 02 Jul 2010 17:27:44 +0200 |
haftmann |
references to ghc and ocaml
|
changeset |
files
|
| Fri, 02 Jul 2010 17:27:44 +0200 |
haftmann |
explicit code_datatype declaration prevents multiple instantiations later on
|
changeset |
files
|
| Fri, 02 Jul 2010 16:50:53 +0200 |
haftmann |
refrain from using datatype declaration -- opens chance for quickcheck later on
|
changeset |
files
|
| Fri, 02 Jul 2010 16:50:52 +0200 |
haftmann |
tuned proof
|
changeset |
files
|
| Fri, 02 Jul 2010 16:20:56 +0200 |
haftmann |
reverted to verion from fc27be4c6b1c
|
changeset |
files
|
| Fri, 02 Jul 2010 16:15:49 +0200 |
haftmann |
traceback for error messages
|
changeset |
files
|
| Fri, 02 Jul 2010 16:10:59 +0200 |
haftmann |
accomodate for different behvaiour of nitpick (c.f. also 180e80b4eac1)
|
changeset |
files
|
| Fri, 02 Jul 2010 14:23:18 +0200 |
haftmann |
introduced distinct session HOL-Codegenerator_Test
|
changeset |
files
|
| Fri, 02 Jul 2010 14:23:17 +0200 |
haftmann |
tuned bootstrap files
|
changeset |
files
|
| Fri, 02 Jul 2010 14:23:17 +0200 |
haftmann |
remove codegeneration-related theories from big library theory
|
changeset |
files
|
| Fri, 02 Jul 2010 14:23:17 +0200 |
haftmann |
drop unconvenient code declarations
|
changeset |
files
|
| Fri, 02 Jul 2010 14:23:16 +0200 |
haftmann |
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
|
changeset |
files
|
| Sun, 04 Jul 2010 21:01:22 +0200 |
wenzelm |
general Future.report -- also for Toplevel.async_state;
|
changeset |
files
|
| Sun, 04 Jul 2010 00:05:32 +0200 |
wenzelm |
simplified Isabelle_Process.Result: use markup directly;
|
changeset |
files
|