src/HOL/Code_Evaluation.thy
Mon, 20 Sep 2010 18:43:23 +0200 haftmann dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
Mon, 20 Sep 2010 15:10:21 +0200 haftmann Factored out ML into separate file
Thu, 16 Sep 2010 16:51:33 +0200 haftmann adjusted to changes in Code_Runtime
Wed, 15 Sep 2010 15:40:35 +0200 haftmann Code_Runtime.value, corresponding to ML_Context.value
Wed, 15 Sep 2010 15:31:32 +0200 haftmann code_eval renamed to code_runtime
Wed, 15 Sep 2010 11:30:31 +0200 haftmann replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references; tuned structures
Fri, 10 Sep 2010 10:59:09 +0200 bulwahn fiddling with the correct setup for String.literal
Fri, 27 Aug 2010 19:34:23 +0200 haftmann renamed class/constant eq to equal; tuned some instantiations
Wed, 11 Aug 2010 14:31:43 +0200 haftmann moved instantiation target formally to class_target.ML
Fri, 16 Apr 2010 21:28:09 +0200 wenzelm replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
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;
Wed, 24 Feb 2010 14:19:52 +0100 haftmann evaluation for abstypes
Mon, 22 Feb 2010 11:10:20 +0100 haftmann proper distinction of code datatypes and abstypes
Mon, 07 Dec 2009 16:27:48 +0100 haftmann split off evaluation mechanisms in separte module Code_Eval
Thu, 12 Nov 2009 15:48:44 +0100 haftmann repaired broken code_const for term_of [String.literal]
Tue, 10 Nov 2009 16:04:57 +0100 wenzelm modernized structure Theory_Target;
Fri, 06 Nov 2009 08:11:58 +0100 bulwahn adding tracing function for evaluated code; annotated compilation in the predicate compiler
Tue, 29 Sep 2009 16:24:36 +0200 wenzelm explicit indication of Unsynchronized.ref;
Wed, 23 Sep 2009 14:00:12 +0200 haftmann Code_Eval(uation)
less more (0) tip