src/Tools/nbe.ML
Fri, 01 Jul 2011 15:16:03 +0200 wenzelm proper @{binding} antiquotations (relevant for formal references);
Thu, 09 Jun 2011 20:22:22 +0200 wenzelm tuned signature: Name.invent and Name.invent_names;
Thu, 09 Jun 2011 15:38:49 +0200 wenzelm prefer new-style Name.invents;
Tue, 19 Apr 2011 20:47:02 +0200 wenzelm split Type_Infer into early and late part, after Proof_Context;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Sat, 08 Jan 2011 17:14:48 +0100 wenzelm misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
Tue, 21 Dec 2010 09:18:29 +0100 haftmann canonical handling of theory context argument
Fri, 17 Dec 2010 18:24:44 +0100 haftmann avoid slightly odd Conv.tap_thy
Wed, 15 Dec 2010 09:47:12 +0100 haftmann simplified evaluation function names
Mon, 13 Dec 2010 22:54:47 +0100 haftmann separated dictionary weakning into separate type
Thu, 09 Dec 2010 17:25:43 +0100 haftmann dictionary constants must permit explicit weakening of classes;
Tue, 07 Dec 2010 21:32:47 +0100 haftmann tuned whitespace
Tue, 07 Dec 2010 09:36:12 +0100 haftmann removed experimental equality checking of closures; acknowledge underapproximation of equality in function name
Fri, 26 Nov 2010 23:13:58 +0100 haftmann nbe decides equality of abstractions by extensionality
Tue, 16 Nov 2010 10:33:36 +0100 haftmann added forall2 predicate lifter
Thu, 04 Nov 2010 17:27:38 +0100 haftmann Code.check_const etc.: reject too specific types
Fri, 01 Oct 2010 17:06:49 +0200 haftmann moved ML_Context.value to Code_Runtime
Tue, 21 Sep 2010 15:46:06 +0200 haftmann no_frees_* is subsumed by new framework mechanisms in Code_Preproc
Thu, 16 Sep 2010 16:51:34 +0200 haftmann separation of static and dynamic thy context
Thu, 16 Sep 2010 08:18:34 +0200 haftmann tuned whitespace
Wed, 15 Sep 2010 15:11:40 +0200 haftmann static nbe conversion
Wed, 15 Sep 2010 13:44:11 +0200 haftmann dropped redundant normal_form command
Wed, 15 Sep 2010 12:11:11 +0200 haftmann more clear separation of static compilation and dynamic evaluation
Wed, 15 Sep 2010 11:30:32 +0200 haftmann replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
Sun, 12 Sep 2010 20:47:47 +0200 wenzelm load type_infer.ML later -- proper context for Type_Infer.infer_types;
Sun, 12 Sep 2010 19:04:02 +0200 wenzelm eliminated aliases of Type.constraint;
Sun, 05 Sep 2010 21:41:24 +0200 wenzelm turned show_sorts/show_types into proper configuration options;
Tue, 31 Aug 2010 16:23:58 +0200 haftmann evaluate takes ml context and ml expression parameter
Tue, 24 Aug 2010 09:06:17 +0200 haftmann tuned
Mon, 23 Aug 2010 11:51:33 +0200 haftmann use conv alias
Mon, 23 Aug 2010 11:09:49 +0200 haftmann refined and unified naming convention for dynamic code evaluation techniques
Thu, 17 Jun 2010 15:59:47 +0200 haftmann more precise code
Thu, 17 Jun 2010 11:33:04 +0200 haftmann transitive superclasses were also only a misunderstanding
Thu, 17 Jun 2010 10:57:00 +0200 haftmann formal introduction of transitive superclasses
Thu, 17 Jun 2010 10:51:38 +0200 haftmann dropped obscure type argument weakening mapping -- was only a misunderstanding
Tue, 15 Jun 2010 14:28:22 +0200 haftmann added code_simp infrastructure
Tue, 15 Jun 2010 08:32:32 +0200 haftmann formal introduction of case cong
Mon, 07 Jun 2010 13:42:38 +0200 haftmann more consistent naming aroud type classes and instances
Thu, 27 May 2010 18:10:37 +0200 wenzelm renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
Thu, 27 May 2010 17:41:27 +0200 wenzelm renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
Wed, 19 May 2010 10:14:37 +0200 haftmann new version of triv_of_class machinery without legacy_unconstrain
Mon, 17 May 2010 23:54:15 +0200 wenzelm prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
Sun, 09 May 2010 22:06:24 +0200 wenzelm reactivated Thm.legacy_unconstrainT for Nbe.lift_triv_classes_conv;
Sun, 09 May 2010 19:15:21 +0200 wenzelm just one version of Thm.unconstrainT, which affects all variables;
Mon, 03 May 2010 20:13:36 +0200 wenzelm renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
Mon, 03 May 2010 14:25:56 +0200 wenzelm renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
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;
Tue, 02 Mar 2010 15:39:06 +0100 haftmann dropped superfluous naming
Wed, 24 Feb 2010 14:19:54 +0100 haftmann tuned whitespace
Mon, 04 Jan 2010 16:00:24 +0100 haftmann code cache only persists on equal theories
Mon, 04 Jan 2010 14:09:56 +0100 haftmann code cache without copy; tuned
Wed, 23 Dec 2009 08:31:15 +0100 haftmann reduced code generator cache to the baremost minimum
Sun, 08 Nov 2009 18:43:42 +0100 wenzelm adapted Theory_Data;
Mon, 19 Oct 2009 21:54:57 +0200 wenzelm uniform use of Integer.add/mult/sum/prod;
Sat, 17 Oct 2009 15:57:51 +0200 wenzelm indicate CRITICAL nature of various setmp combinators;
Tue, 29 Sep 2009 16:24:36 +0200 wenzelm explicit indication of Unsynchronized.ref;
Wed, 09 Sep 2009 11:31:20 +0200 haftmann moved eq handling in nbe into separate oracle
Tue, 21 Jul 2009 15:44:31 +0200 haftmann integrated add_triv_classes into evaluation stack
Wed, 08 Jul 2009 08:18:07 +0200 haftmann tuned structure Code internally
Tue, 07 Jul 2009 17:21:27 +0200 haftmann tuned interface of structure Code
less more (0) -100 -60 tip