| Fri, 04 Dec 2009 15:20:24 +0100 |
wenzelm |
merged, resolving minor conflicts;
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 12:22:09 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 30 Nov 2009 12:28:12 +0100 |
haftmann |
dropped some unused bindings
|
file |
diff |
annotate
|
| Wed, 25 Nov 2009 09:13:46 +0100 |
haftmann |
normalized uncurry take/drop
|
file |
diff |
annotate
|
| Tue, 24 Nov 2009 17:28:25 +0100 |
haftmann |
curried take/drop
|
file |
diff |
annotate
|
| Wed, 02 Dec 2009 17:53:35 +0100 |
haftmann |
crude support for type aliasses and corresponding constant signatures
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 08:25:57 +0100 |
bulwahn |
replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules
|
file |
diff |
annotate
|
| Mon, 16 Nov 2009 10:16:40 +0100 |
haftmann |
proper purge
|
file |
diff |
annotate
|
| Mon, 09 Nov 2009 14:47:16 +0100 |
haftmann |
tuned error messages; tuned code
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 18:43:42 +0100 |
wenzelm |
adapted Theory_Data;
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 16:15:33 +0100 |
wenzelm |
modernized functor/structures Interpretation;
|
file |
diff |
annotate
|
| Thu, 22 Oct 2009 16:50:24 +0200 |
haftmann |
close thm derivations explicitly
|
file |
diff |
annotate
|
| Mon, 19 Oct 2009 16:34:12 +0200 |
haftmann |
dropped lazy code equations
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 15:57:51 +0200 |
wenzelm |
indicate CRITICAL nature of various setmp combinators;
|
file |
diff |
annotate
|
| Wed, 14 Oct 2009 13:56:56 +0200 |
haftmann |
sharpened name
|
file |
diff |
annotate
|
| Wed, 14 Oct 2009 12:20:01 +0200 |
haftmann |
more explicit notion of canonized code equations
|
file |
diff |
annotate
|
| Mon, 05 Oct 2009 15:04:45 +0200 |
haftmann |
tuned handling of type variable names further
|
file |
diff |
annotate
|
| Mon, 05 Oct 2009 08:36:33 +0200 |
haftmann |
variables in type schemes must be renamed simultaneously with variables in equations
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
handling of definitions
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
experimenting to add some useful interface for definitions
|
file |
diff |
annotate
|
| Tue, 22 Sep 2009 08:58:08 +0200 |
haftmann |
corrected order of type variables in code equations; more precise certificate for cases
|
file |
diff |
annotate
|
| Wed, 09 Sep 2009 11:31:20 +0200 |
haftmann |
moved eq handling in nbe into separate oracle
|
file |
diff |
annotate
|
| Mon, 10 Aug 2009 12:25:30 +0200 |
haftmann |
same_typscheme replaces ugly common_typ_eqns
|
file |
diff |
annotate
|
| Fri, 31 Jul 2009 09:46:09 +0200 |
haftmann |
using certify_instantiate
|
file |
diff |
annotate
|
| Fri, 31 Jul 2009 09:34:05 +0200 |
haftmann |
cleaned up variable desymbolification and argument expansion
|
file |
diff |
annotate
|
| Wed, 22 Jul 2009 11:23:09 +0200 |
wenzelm |
merged, resolving trivial conflict;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 15:44:31 +0200 |
haftmann |
more accurate check of judgment type
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 01:03:18 +0200 |
wenzelm |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 16:27:33 +0200 |
haftmann |
clarified code
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 10:54:04 +0200 |
haftmann |
code attributes use common underscore convention
|
file |
diff |
annotate
|
| Thu, 09 Jul 2009 22:01:41 +0200 |
wenzelm |
renamed functor TableFun to Table, and GraphFun to Graph;
|
file |
diff |
annotate
|
| Wed, 08 Jul 2009 08:18:07 +0200 |
haftmann |
tuned structure Code internally
|
file |
diff |
annotate
|
| Tue, 07 Jul 2009 17:21:27 +0200 |
haftmann |
tuned interface of structure Code
|
file |
diff |
annotate
|
| Tue, 30 Jun 2009 18:23:50 +0200 |
haftmann |
an intermediate step towards a refined translation of cases
|
file |
diff |
annotate
|
| Mon, 15 Jun 2009 16:13:04 +0200 |
haftmann |
permissive code attribute; all_eqns
|
file |
diff |
annotate
|
| Tue, 09 Jun 2009 22:59:55 +0200 |
haftmann |
tuned make/map/merge combinators
|
file |
diff |
annotate
|
| Thu, 14 May 2009 15:09:48 +0200 |
haftmann |
merged module code_unit.ML into code.ML
|
file |
diff |
annotate
|
| Thu, 14 May 2009 09:16:36 +0200 |
haftmann |
strip sorts while checking pattern subsumption
|
file |
diff |
annotate
|
| Tue, 12 May 2009 19:30:33 +0200 |
haftmann |
transferred code generator preprocessor into separate module
|
file |
diff |
annotate
|
| Mon, 11 May 2009 11:53:21 +0200 |
haftmann |
corrected deletetion of code equations for constructors
|
file |
diff |
annotate
|
| Mon, 11 May 2009 10:53:19 +0200 |
haftmann |
clarified matter of "proper" flag in code equations
|
file |
diff |
annotate
|
| Mon, 11 May 2009 09:40:38 +0200 |
haftmann |
clarified terminilogy concerning nbe equations
|
file |
diff |
annotate
|
| Wed, 15 Apr 2009 15:38:30 +0200 |
haftmann |
say farewell to code related to old code_funcgr module
|
file |
diff |
annotate
|
| Thu, 26 Mar 2009 14:14:02 +0100 |
wenzelm |
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
|
file |
diff |
annotate
|
| Sun, 15 Mar 2009 15:59:44 +0100 |
wenzelm |
simplified attribute setup;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 21:25:15 +0100 |
wenzelm |
eliminated type Args.T;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 12:16:12 +0100 |
wenzelm |
proper context for Simplifier.pretty_ss;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Mon, 23 Feb 2009 21:38:36 +0100 |
haftmann |
improved treatment of case certificates
|
file |
diff |
annotate
|
| Sun, 22 Feb 2009 18:00:05 +0100 |
haftmann |
subalgebra: drop arities if desired
|
file |
diff |
annotate
|
| Fri, 20 Feb 2009 18:29:10 +0100 |
haftmann |
permissive check for pattern discipline in case schemes
|
file |
diff |
annotate
|
| Wed, 18 Feb 2009 19:18:32 +0100 |
haftmann |
tuned accessor name
|
file |
diff |
annotate
|
| Thu, 01 Jan 2009 23:31:49 +0100 |
wenzelm |
normalized some ML type/val aliases;
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 23:00:21 +0100 |
wenzelm |
renamed type Lazy.T to lazy;
|
file |
diff |
annotate
|
| Wed, 29 Oct 2008 11:33:40 +0100 |
haftmann |
explicit check for pattern discipline before code translation
|
file |
diff |
annotate
|
| Tue, 28 Oct 2008 16:58:59 +0100 |
haftmann |
cleanup code default attribute
|
file |
diff |
annotate
|
| Mon, 27 Oct 2008 16:15:50 +0100 |
haftmann |
explicit history for equations; tuned
|
file |
diff |
annotate
|
| Thu, 23 Oct 2008 14:22:16 +0200 |
wenzelm |
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
|
file |
diff |
annotate
|
| Thu, 23 Oct 2008 13:52:28 +0200 |
wenzelm |
adapted Susp.peek;
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Tue, 07 Oct 2008 16:07:59 +0200 |
haftmann |
clarified preprocessor policies
|
file |
diff |
annotate
|
| Tue, 30 Sep 2008 12:49:18 +0200 |
haftmann |
clarified codegen interfaces
|
file |
diff |
annotate
|
| Mon, 29 Sep 2008 12:32:00 +0200 |
haftmann |
more precise redundancy check
|
file |
diff |
annotate
|
| Fri, 26 Sep 2008 09:09:52 +0200 |
haftmann |
clarified function transformator interface
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 16:05:52 +0200 |
haftmann |
clarifed redundancy policy
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 11:14:01 +0200 |
haftmann |
(temporary workaround)
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 09:28:08 +0200 |
haftmann |
non left-linear equations for nbe
|
file |
diff |
annotate
|
| Fri, 05 Sep 2008 06:50:22 +0200 |
haftmann |
different bookkeeping for code equations
|
file |
diff |
annotate
|
| Thu, 28 Aug 2008 22:09:20 +0200 |
haftmann |
restructured and split code serializer module
|
file |
diff |
annotate
|
| Sun, 24 Aug 2008 14:42:26 +0200 |
haftmann |
corrected cache handling for class operations
|
file |
diff |
annotate
|
| Mon, 21 Jul 2008 15:26:26 +0200 |
haftmann |
added explicit purge_data
|
file |
diff |
annotate
|
| Tue, 15 Jul 2008 16:02:07 +0200 |
haftmann |
tuned code theorem bookkeeping
|
file |
diff |
annotate
|
| Mon, 14 Jul 2008 19:20:57 +0200 |
haftmann |
dropped junk
|
file |
diff |
annotate
|
| Mon, 14 Jul 2008 11:04:46 +0200 |
haftmann |
simpsets as pre/postprocessors; generic preprocessor now named function transformators
|
file |
diff |
annotate
|
| Fri, 23 May 2008 16:05:07 +0200 |
haftmann |
explicit type schemes for functions
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:04:37 +0200 |
wenzelm |
moved global pretty/string_of functions from Sign to Syntax;
|
file |
diff |
annotate
|
| Sat, 17 May 2008 13:54:30 +0200 |
wenzelm |
structure Display: less pervasive operations;
|
file |
diff |
annotate
|
| Fri, 28 Mar 2008 20:02:04 +0100 |
wenzelm |
Context.>> : operate on Context.generic;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 15:32:15 +0100 |
wenzelm |
eliminated delayed theory setup
|
file |
diff |
annotate
|
| Thu, 31 Jan 2008 11:44:46 +0100 |
haftmann |
explicit del_funcs
|
file |
diff |
annotate
|
| Fri, 25 Jan 2008 14:54:48 +0100 |
haftmann |
print postprocessor equations
|
file |
diff |
annotate
|
| Mon, 10 Dec 2007 11:24:15 +0100 |
haftmann |
moved instance parameter management from class.ML to axclass.ML
|
file |
diff |
annotate
|
| Thu, 29 Nov 2007 07:55:46 +0100 |
haftmann |
dropped dead code
|
file |
diff |
annotate
|
| Wed, 28 Nov 2007 09:01:42 +0100 |
haftmann |
tuned interfaces of class module
|
file |
diff |
annotate
|
| Fri, 23 Nov 2007 21:09:35 +0100 |
haftmann |
rudimentary instantiation target
|
file |
diff |
annotate
|
| Tue, 06 Nov 2007 13:12:55 +0100 |
haftmann |
clarified merge
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 16:05:47 +0200 |
wenzelm |
removed obsolete AxClass.params_of_class;
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 17:10:38 +0200 |
wenzelm |
renamed AxClass.get_definition to AxClass.get_info (again);
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 20:29:24 +0200 |
wenzelm |
replaced literal 'a by Name.aT;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 19:54:44 +0200 |
haftmann |
certificates for code generator case expressions
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 19:41:51 +0200 |
haftmann |
clarified terminology
|
file |
diff |
annotate
|
| Wed, 26 Sep 2007 20:50:33 +0200 |
wenzelm |
Sign.minimize/complete_sort;
|
file |
diff |
annotate
|
| Thu, 20 Sep 2007 16:37:31 +0200 |
haftmann |
more permissive
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 07:36:15 +0200 |
haftmann |
distinction between regular and default code theorems
|
file |
diff |
annotate
|
| Sat, 15 Sep 2007 19:27:40 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 24 Aug 2007 14:14:20 +0200 |
haftmann |
overloaded definitions accompanied by explicit constants
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 08:57:42 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 10 Aug 2007 17:04:34 +0200 |
haftmann |
new structure for code generator modules
|
file |
diff |
annotate
|