| Mon, 23 Aug 2010 11:51:32 +0200 |
haftmann |
preliminary versions of static_eval_conv(_simple)
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 11:09:49 +0200 |
haftmann |
refined and unified naming convention for dynamic code evaluation techniques
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 15:31:38 +0200 |
wenzelm |
replaced Thy_Info.the_theory by Context.this_theory -- avoid referring to accidental theory loader state;
|
file |
diff |
annotate
|
| Fri, 16 Jul 2010 13:57:46 +0200 |
haftmann |
don't fail gracefully
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
tuned titles
|
file |
diff |
annotate
|
| Mon, 05 Jul 2010 10:39:49 +0200 |
haftmann |
dropped passed irregular names
|
file |
diff |
annotate
|
| Fri, 02 Jul 2010 16:20:56 +0200 |
haftmann |
reverted to verion from fc27be4c6b1c
|
file |
diff |
annotate
|
| Fri, 02 Jul 2010 16:15:49 +0200 |
haftmann |
traceback for error messages
|
file |
diff |
annotate
|
| Wed, 30 Jun 2010 11:38:51 +0200 |
haftmann |
unfold_fun_n
|
file |
diff |
annotate
|
| Thu, 17 Jun 2010 15:59:46 +0200 |
haftmann |
explicit type variable arguments for constructors
|
file |
diff |
annotate
|
| Thu, 17 Jun 2010 11:33:04 +0200 |
haftmann |
transitive superclasses were also only a misunderstanding
|
file |
diff |
annotate
|
| Thu, 17 Jun 2010 10:57:00 +0200 |
haftmann |
formal introduction of transitive superclasses
|
file |
diff |
annotate
|
| Thu, 17 Jun 2010 10:51:38 +0200 |
haftmann |
dropped obscure type argument weakening mapping -- was only a misunderstanding
|
file |
diff |
annotate
|
| Tue, 15 Jun 2010 11:38:40 +0200 |
haftmann |
maintain cong rules for case combinators; more precise permissiveness
|
file |
diff |
annotate
|
| Tue, 15 Jun 2010 08:32:32 +0200 |
haftmann |
formal introduction of case cong
|
file |
diff |
annotate
|
| Mon, 14 Jun 2010 16:00:47 +0200 |
haftmann |
teaked naming of superclass projections
|
file |
diff |
annotate
|
| Mon, 07 Jun 2010 13:42:38 +0200 |
haftmann |
more consistent naming aroud type classes and instances
|
file |
diff |
annotate
|
| Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| Wed, 21 Apr 2010 15:20:59 +0200 |
haftmann |
optionally ignore errors during translation of equations; tuned representation of abstraction points
|
file |
diff |
annotate
|
| Mon, 19 Apr 2010 15:31:58 +0200 |
haftmann |
more appropriate representation of valid positions for abstractors
|
file |
diff |
annotate
|
| Sun, 11 Apr 2010 13:08:14 +0200 |
wenzelm |
of_sort_derivation: pass-through full type information -- following the version by krauss/schropp;
|
file |
diff |
annotate
|
| Thu, 25 Mar 2010 21:27:04 +0100 |
wenzelm |
Sorts.of_sort_derivation: do not use slow Graph.irreducible_paths here, which not always needed (SUBTLE CHANGE IN SEMANTICS);
|
file |
diff |
annotate
|
| Sat, 20 Mar 2010 17:33:11 +0100 |
wenzelm |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file |
diff |
annotate
|
| Mon, 22 Feb 2010 11:10:20 +0100 |
haftmann |
proper distinction of code datatypes and abstypes
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 11:06:21 +0100 |
haftmann |
a simple concept for datatype invariants
|
file |
diff |
annotate
|
| Wed, 13 Jan 2010 12:20:37 +0100 |
haftmann |
explicit abstract type of code certificates
|
file |
diff |
annotate
|
| Tue, 12 Jan 2010 16:27:42 +0100 |
haftmann |
code certificates as integral part of code generation
|
file |
diff |
annotate
|
| Mon, 04 Jan 2010 16:00:24 +0100 |
haftmann |
code cache only persists on equal theories
|
file |
diff |
annotate
|
| Mon, 04 Jan 2010 14:09:56 +0100 |
haftmann |
code cache without copy; tuned
|
file |
diff |
annotate
|
| Wed, 23 Dec 2009 08:31:15 +0100 |
haftmann |
reduced code generator cache to the baremost minimum
|
file |
diff |
annotate
|
| Mon, 14 Dec 2009 10:23:25 +0100 |
haftmann |
explicit name for function space
|
file |
diff |
annotate
|
| Mon, 07 Dec 2009 09:16:27 +0100 |
haftmann |
repaired read_const_expr, broken in 1e7ca47c6c3d
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 18:51:15 +0100 |
haftmann |
merged, resolving minor conflicts
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 18:19:31 +0100 |
haftmann |
avoid misleading name "superarities"
|
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:36 +0100 |
haftmann |
subst_signatures
|
file |
diff |
annotate
|
| Tue, 03 Nov 2009 17:06:08 +0100 |
haftmann |
pretty name for ==>
|
file |
diff |
annotate
|
| Mon, 26 Oct 2009 10:51:42 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 20:54:21 +0100 |
wenzelm |
maintain theory name via name space, not tags;
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 20:54:31 +0200 |
wenzelm |
uniform use of Integer.min/max;
|
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, 12 Oct 2009 16:16:44 +0200 |
haftmann |
added add_tyconames; tuned
|
file |
diff |
annotate
|
| Mon, 12 Oct 2009 12:19:19 +0200 |
haftmann |
added is_IVar
|
file |
diff |
annotate
|
| Thu, 08 Oct 2009 15:59:17 +0200 |
haftmann |
added group_stmts
|
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
|
| Wed, 30 Sep 2009 23:30:37 +0200 |
wenzelm |
Sorts.of_sort_derivation: no pp here;
|
file |
diff |
annotate
|
| Wed, 09 Sep 2009 12:27:12 +0200 |
haftmann |
explicit transfer avoids spurious merge problems
|
file |
diff |
annotate
|
| Tue, 11 Aug 2009 10:43:43 +0200 |
haftmann |
proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
|
file |
diff |
annotate
|
| Mon, 10 Aug 2009 12:24:49 +0200 |
haftmann |
moved all technical processing of code equations to code_thingol.ML
|
file |
diff |
annotate
|
| Mon, 10 Aug 2009 08:37:37 +0200 |
haftmann |
attempt to move desymbolization to translation
|
file |
diff |
annotate
|
| Wed, 29 Jul 2009 16:42:47 +0200 |
haftmann |
abstractions: desymbolize name hint
|
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 |
integrated add_triv_classes into evaluation stack
|
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
|