src/HOL/Code_Evaluation.thy
Sun, 15 Nov 2020 07:17:06 +0000 haftmann bundles for reflected term syntax
Sun, 06 Jan 2019 15:04:34 +0100 wenzelm isabelle update -u path_cartouches;
Tue, 24 Apr 2018 14:17:58 +0000 haftmann proper datatype for 8-bit characters
Mon, 05 Jun 2017 15:59:45 +0200 haftmann streamlined code setup for fake terms
Mon, 05 Sep 2016 23:11:00 +0200 wenzelm clarified modules;
Thu, 26 May 2016 15:27:50 +0200 haftmann delegate inclusion of required dictionaries to user-space instead of half-working magic
Tue, 12 Apr 2016 14:38:57 +0200 wenzelm Type_Infer.object_logic controls improvement of type inference result;
Sat, 12 Mar 2016 22:04:52 +0100 haftmann model characters directly as range 0..255
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Thu, 05 Feb 2015 19:44:14 +0100 haftmann slightly more standard code setup for String.literal, with explicit special case in predicate compiler
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Tue, 16 Sep 2014 19:23:37 +0200 blanchet added 'extraction' plugins -- this might help 'HOL-Proofs'
Sun, 14 Sep 2014 22:59:30 +0200 blanchet disable datatype 'plugins' for internal types
Thu, 11 Sep 2014 19:32:36 +0200 blanchet updated news
Wed, 03 Sep 2014 00:06:24 +0200 blanchet use 'datatype_new' in 'Main'
Mon, 25 Aug 2014 09:08:45 +0200 Andreas Lochbihler correct code equation for term_of on integer
Fri, 22 Aug 2014 14:39:40 +0200 Andreas Lochbihler add code equation for term_of on integer
Fri, 09 May 2014 08:13:37 +0200 haftmann dropped term_of obfuscation -- not really required;
Fri, 09 May 2014 08:13:37 +0200 haftmann hardcoded nbe and sml into value command
Fri, 09 May 2014 08:13:36 +0200 haftmann modernized setups
Fri, 09 May 2014 08:13:36 +0200 haftmann degeneralized value command into HOL
Fri, 21 Mar 2014 11:42:32 +0100 wenzelm more qualified names;
Fri, 21 Feb 2014 00:09:56 +0100 blanchet adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
Sun, 23 Jun 2013 21:16:07 +0200 haftmann migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
Sun, 02 Jun 2013 07:46:40 +0200 haftmann make reification part of HOL
Sat, 25 May 2013 15:37:53 +0200 wenzelm syntax translations always depend on context;
Fri, 15 Feb 2013 11:47:33 +0100 haftmann systematic conversions between nat and nibble/char;
Fri, 15 Feb 2013 08:31:31 +0100 haftmann less customary term_of conversions;
Fri, 15 Feb 2013 08:31:31 +0100 haftmann two target language numeral types: integer and natural, as replacement for code_numeral;
Thu, 14 Feb 2013 15:27:10 +0100 haftmann reform of predicate compiler / quickcheck theories:
Thu, 14 Feb 2013 12:24:42 +0100 haftmann abandoned theory Plain
Mon, 12 Nov 2012 23:24:40 +0100 haftmann tuned import order
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Fri, 24 Feb 2012 22:46:44 +0100 haftmann moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
Fri, 24 Feb 2012 09:40:02 +0100 haftmann given up disfruitful branch
Thu, 23 Feb 2012 21:25:59 +0100 haftmann moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
Thu, 26 May 2011 09:42:02 +0200 bulwahn extending terms of Code_Evaluation by Free to allow partial terms
Thu, 02 Dec 2010 14:34:38 +0100 haftmann corrected representation for code_numeral numerals
Thu, 02 Dec 2010 13:53:36 +0100 haftmann separate term_of function for integers -- more canonical representation of negative integers
Mon, 22 Nov 2010 10:41:57 +0100 bulwahn adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict
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
less more (0) -60 tip