Wed, 12 Nov 2008 17:23:22 +0100 |
krauss |
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
|
changeset |
files
|
Mon, 10 Nov 2008 19:42:22 +0100 |
haftmann |
restruced naming code in anticipation of introduction of name morphisms
|
changeset |
files
|
Mon, 10 Nov 2008 19:42:21 +0100 |
haftmann |
more verbose element printing
|
changeset |
files
|
Mon, 10 Nov 2008 19:42:20 +0100 |
haftmann |
clarified comment
|
changeset |
files
|
Mon, 10 Nov 2008 17:38:23 +0100 |
berghofe |
Added support for parametric datatypes.
|
changeset |
files
|
Mon, 10 Nov 2008 17:37:25 +0100 |
berghofe |
Streamlined functions for accessing information about atoms.
|
changeset |
files
|
Mon, 10 Nov 2008 17:34:26 +0100 |
berghofe |
Some more functions for accessing information about atoms.
|
changeset |
files
|
Mon, 10 Nov 2008 14:36:49 +0100 |
ballarin |
Made doc compatible with the system.
|
changeset |
files
|
Mon, 10 Nov 2008 09:03:28 +0100 |
haftmann |
clarified verbatim vs. typewriter
|
changeset |
files
|
Mon, 10 Nov 2008 08:18:58 +0100 |
haftmann |
using explicit interpretaton prefix in Name.binding (still on the surface)
|
changeset |
files
|
Mon, 10 Nov 2008 08:18:57 +0100 |
haftmann |
explicit interpretation prefix in Name.binding
|
changeset |
files
|
Mon, 10 Nov 2008 08:18:56 +0100 |
haftmann |
tuned
|
changeset |
files
|
Fri, 07 Nov 2008 08:57:15 +0100 |
haftmann |
exported codegen_preproc
|
changeset |
files
|
Thu, 06 Nov 2008 12:30:49 +0100 |
ballarin |
Minor cleanup.
|
changeset |
files
|
Thu, 06 Nov 2008 12:29:51 +0100 |
ballarin |
Keyword 'includes' gone.
|
changeset |
files
|
Thu, 06 Nov 2008 11:52:50 +0100 |
nipkow |
tuned
|
changeset |
files
|
Thu, 06 Nov 2008 11:52:42 +0100 |
nipkow |
added lemma
|
changeset |
files
|
Thu, 06 Nov 2008 10:05:48 +0100 |
nipkow |
Added second tiling example.
|
changeset |
files
|
Thu, 06 Nov 2008 09:09:51 +0100 |
haftmann |
cleaned
|
changeset |
files
|
Thu, 06 Nov 2008 09:09:49 +0100 |
haftmann |
tuned
|
changeset |
files
|
Thu, 06 Nov 2008 09:09:48 +0100 |
haftmann |
class morphism stemming from locale interpretation
|
changeset |
files
|
Mon, 03 Nov 2008 14:15:25 +0100 |
haftmann |
improved verbatim mechanism
|
changeset |
files
|
Fri, 31 Oct 2008 10:39:04 +0100 |
berghofe |
Theorem "_" is now stored with open derivation.
|
changeset |
files
|
Fri, 31 Oct 2008 10:37:34 +0100 |
berghofe |
Removed argument prf2 in rewrite rules for equal_elim to make them applicable
|
changeset |
files
|
Fri, 31 Oct 2008 10:35:30 +0100 |
berghofe |
Replaced arbitrary by undefined.
|
changeset |
files
|
Thu, 30 Oct 2008 10:57:45 +0100 |
ballarin |
Dropped context element 'includes'.
|
changeset |
files
|
Wed, 29 Oct 2008 15:32:58 +0100 |
haftmann |
adapted to strict pattern discipline
|
changeset |
files
|
Wed, 29 Oct 2008 11:33:40 +0100 |
haftmann |
explicit check for pattern discipline before code translation
|
changeset |
files
|