| Tue, 09 Aug 2011 07:37:18 -0700 |
huffman |
Derivative.thy: clean up formatting
|
changeset |
files
|
| Mon, 08 Aug 2011 21:17:52 -0700 |
huffman |
instance real_basis_with_inner < perfect_space
|
changeset |
files
|
| Wed, 10 Aug 2011 20:53:43 +0200 |
wenzelm |
old term operations are legacy;
|
changeset |
files
|
| Wed, 10 Aug 2011 20:12:36 +0200 |
wenzelm |
moved old code generator to src/Tools/;
|
changeset |
files
|
| Wed, 10 Aug 2011 19:46:48 +0200 |
wenzelm |
avoid OldTerm operations -- with subtle changes of semantics;
|
changeset |
files
|
| Wed, 10 Aug 2011 19:45:57 +0200 |
wenzelm |
avoid OldTerm operations -- with subtle changes of semantics;
|
changeset |
files
|
| Wed, 10 Aug 2011 19:45:41 +0200 |
wenzelm |
avoid OldTerm operations -- with subtle changes of semantics;
|
changeset |
files
|
| Wed, 10 Aug 2011 19:21:28 +0200 |
wenzelm |
avoid OldTerm operations -- with subtle changes of semantics;
|
changeset |
files
|
| Wed, 10 Aug 2011 16:26:05 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 10 Aug 2011 16:24:39 +0200 |
wenzelm |
Goal.forked: clarified handling of interrupts;
|
changeset |
files
|
| Wed, 10 Aug 2011 16:05:14 +0200 |
wenzelm |
future_job: explicit indication of interrupts;
|
changeset |
files
|
| Wed, 10 Aug 2011 15:17:24 +0200 |
wenzelm |
more explicit Simple_Thread.interrupt_unsynchronized, to emphasize its meaning;
|
changeset |
files
|