| Thu, 13 Nov 2008 15:58:37 +0100 |
haftmann |
improved handling of !!/==> for eval and normalization
|
changeset |
files
|
| Thu, 13 Nov 2008 14:19:10 +0100 |
haftmann |
proper name morphisms for locales
|
changeset |
files
|
| Thu, 13 Nov 2008 14:19:09 +0100 |
haftmann |
consider prefixes for name bindings of simprocs (a first approximation)
|
changeset |
files
|
| Thu, 13 Nov 2008 14:19:07 +0100 |
haftmann |
diagnostic output for name bindings
|
changeset |
files
|
| Thu, 13 Nov 2008 01:31:20 +0100 |
berghofe |
Some modifications in code for proving arities to make it work for datatype
|
changeset |
files
|
| 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
|
| Tue, 28 Oct 2008 17:53:46 +0100 |
ballarin |
Revoked workaround (incompatible with HOL/ex/LocaleTest2.thy).
|
changeset |
files
|
| Tue, 28 Oct 2008 16:59:02 +0100 |
haftmann |
restored incremental code generation
|
changeset |
files
|
| Tue, 28 Oct 2008 16:59:01 +0100 |
haftmann |
slightly tuned
|
changeset |
files
|
| Tue, 28 Oct 2008 16:59:00 +0100 |
haftmann |
assert that no class parameter is used as constructor
|
changeset |
files
|
| Tue, 28 Oct 2008 16:58:59 +0100 |
haftmann |
cleanup code default attribute
|
changeset |
files
|
| Tue, 28 Oct 2008 12:29:57 +0100 |
haftmann |
removed includes
|
changeset |
files
|
| Tue, 28 Oct 2008 12:28:14 +0100 |
haftmann |
making SMLNJ happy
|
changeset |
files
|
| Tue, 28 Oct 2008 11:05:44 +0100 |
paulson |
The metis method no longer fails because the theorem is too trivial
|
changeset |
files
|
| Tue, 28 Oct 2008 11:03:07 +0100 |
ballarin |
Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.
|
changeset |
files
|
| Mon, 27 Oct 2008 18:14:34 +0100 |
paulson |
metis proof
|
changeset |
files
|
| Mon, 27 Oct 2008 16:23:54 +0100 |
ballarin |
New-style locale expressions with instantiation (new file expression.ML).
|
changeset |
files
|
| Mon, 27 Oct 2008 16:20:52 +0100 |
ballarin |
Hide path in constant name (workaround).
|
changeset |
files
|
| Mon, 27 Oct 2008 16:15:50 +0100 |
haftmann |
explicit history for equations; tuned
|
changeset |
files
|
| Mon, 27 Oct 2008 16:15:49 +0100 |
haftmann |
slightly tuned
|
changeset |
files
|
| Mon, 27 Oct 2008 16:15:48 +0100 |
haftmann |
added rudimentary code generation
|
changeset |
files
|
| Mon, 27 Oct 2008 16:15:47 +0100 |
haftmann |
sup_bot and inf_top
|
changeset |
files
|
| Mon, 27 Oct 2008 16:14:51 +0100 |
ballarin |
Extension of interface: declarations_of.
|
changeset |
files
|
| Fri, 24 Oct 2008 17:51:36 +0200 |
haftmann |
simplified user-defined class syntax
|
changeset |
files
|
| Fri, 24 Oct 2008 17:51:35 +0200 |
haftmann |
more clever module names for code generation
|
changeset |
files
|
| Fri, 24 Oct 2008 17:48:42 +0200 |
haftmann |
"fun" gained a more uniform status
|
changeset |
files
|
| Fri, 24 Oct 2008 17:48:40 +0200 |
haftmann |
simplified syntax for class parameters
|
changeset |
files
|
| Fri, 24 Oct 2008 17:48:39 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Fri, 24 Oct 2008 17:48:37 +0200 |
haftmann |
new classes "top" and "bot"
|
changeset |
files
|
| Fri, 24 Oct 2008 17:48:36 +0200 |
haftmann |
tuned proof
|
changeset |
files
|
| Fri, 24 Oct 2008 17:48:35 +0200 |
haftmann |
more clever module name aliasses for code generation
|
changeset |
files
|
| Fri, 24 Oct 2008 17:48:34 +0200 |
haftmann |
"arbitrary" merely abbreviates undefined
|
changeset |
files
|
| Fri, 24 Oct 2008 17:48:33 +0200 |
haftmann |
subst is a proper axiom again
|
changeset |
files
|