Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/Code_Generator.thy
Thu, 28 Mar 2019 21:24:55 +0100 wenzelm "export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports; file | diff | annotate
Sun, 06 Jan 2019 15:04:34 +0100 wenzelm isabelle update -u path_cartouches; file | diff | annotate
Mon, 11 Jul 2016 11:15:10 +0200 wenzelm clarified keywords; file | diff | annotate
Fri, 01 Jan 2016 10:49:00 +0100 wenzelm isabelle update_cartouches -c -t; file | diff | annotate
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>; file | diff | annotate
Fri, 09 Jan 2015 08:36:59 +0100 haftmann modernized and more uniform style file | diff | annotate
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section; file | diff | annotate
Sat, 28 Jun 2014 22:13:23 +0200 haftmann tracing facilities for the code generator preprocessor file | diff | annotate
Thu, 15 May 2014 16:38:29 +0200 haftmann modernized setup file | diff | annotate
Fri, 09 May 2014 08:13:36 +0200 haftmann degeneralized value command into HOL file | diff | annotate
Sun, 09 Feb 2014 21:37:27 +0100 haftmann dropped legacy finally file | diff | annotate
Wed, 01 Jan 2014 01:05:48 +0100 haftmann fundamental treatment of undefined vs. universally partial replaces code_abort file | diff | annotate
Fri, 24 May 2013 23:57:24 +0200 haftmann bookkeeping and input syntax for exact specification of names of symbols in generated code file | diff | annotate
Fri, 24 May 2013 23:57:24 +0200 haftmann use generic data for code symbols for unified "code_printing" syntax for custom serialisations file | diff | annotate
Fri, 24 May 2013 23:57:24 +0200 haftmann dedicated module for code symbol data file | diff | annotate
Mon, 25 Feb 2013 13:31:02 +0100 wenzelm reconsider 'export_code' as "thy_decl" command due to its global side-effect on the file-system; file | diff | annotate
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses; file | diff | annotate
Thu, 19 Apr 2012 19:36:24 +0200 haftmann moved modules with only vague relation to the code generator to theory HOL rather than theory Code_Generator file | diff | annotate
Thu, 19 Apr 2012 19:18:47 +0200 haftmann tuned whitespace file | diff | annotate
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure; file | diff | annotate
Thu, 15 Mar 2012 19:02:34 +0100 wenzelm declare minor keywords via theory header; file | diff | annotate
Wed, 19 Oct 2011 09:11:20 +0200 bulwahn removing old code generator file | diff | annotate
Wed, 10 Aug 2011 20:53:43 +0200 wenzelm old term operations are legacy; file | diff | annotate
Wed, 10 Aug 2011 20:12:36 +0200 wenzelm moved old code generator to src/Tools/; file | diff | annotate
Fri, 01 Jul 2011 10:45:49 +0200 bulwahn adding a value antiquotation file | diff | annotate
Mon, 27 Jun 2011 22:20:49 +0200 wenzelm document antiquotations are managed as theory data, with proper name space and entity markup; file | diff | annotate
Fri, 27 May 2011 10:30:08 +0200 blanchet renamed "Auto_Tools" "Try" file | diff | annotate
Mon, 25 Oct 2010 10:30:46 +0200 blanchet introduced manual version of "Auto Solve" as "solve_direct" file | diff | annotate
Fri, 01 Oct 2010 17:06:49 +0200 haftmann moved ML_Context.value to Code_Runtime file | diff | annotate
Thu, 16 Sep 2010 16:51:34 +0200 haftmann adjusted setup file | diff | annotate
Wed, 15 Sep 2010 16:56:31 +0200 haftmann load code_runtime immediately again file | diff | annotate
Wed, 15 Sep 2010 16:47:31 +0200 haftmann introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy file | diff | annotate
Wed, 15 Sep 2010 15:31:32 +0200 haftmann code_eval renamed to code_runtime file | diff | annotate
Sat, 11 Sep 2010 12:32:31 +0200 blanchet make Auto Solve part of the "Auto Tools" file | diff | annotate
Sat, 11 Sep 2010 10:28:44 +0200 blanchet start renaming "Auto_Counterexample" to "Auto_Tools"; file | diff | annotate
Wed, 01 Sep 2010 12:01:19 +0200 haftmann factored out generic part of Scala serializer into code_namespace.ML file | diff | annotate
Wed, 14 Jul 2010 14:16:12 +0200 haftmann load cache_io before code generator; moved adhoc-overloading to generic tools file | diff | annotate
Tue, 15 Jun 2010 14:28:22 +0200 haftmann added code_simp infrastructure file | diff | annotate
Wed, 27 Jan 2010 14:02:52 +0100 haftmann tuned structure; moved non-related quickcheck.setup to Code_Generator.thy file | diff | annotate
Fri, 08 Jan 2010 12:25:15 +0100 haftmann a primitive scala serializer file | diff | annotate
Mon, 07 Dec 2009 16:27:48 +0100 haftmann split off evaluation mechanisms in separte module Code_Eval file | diff | annotate
Tue, 24 Nov 2009 17:19:33 +0100 wenzelm some rearangement of load order to keep preferences adjacent -- slightly fragile; file | diff | annotate
Fri, 20 Nov 2009 15:33:10 +0100 wenzelm load ML directly into theory Code_Generator (quickcheck also requires this); file | diff | annotate
Wed, 28 Oct 2009 17:43:43 +0100 blanchet introduced Auto Nitpick in addition to Auto Quickcheck; file | diff | annotate
Tue, 23 Jun 2009 12:09:30 +0200 haftmann uniformly capitialized names for subdirectories file | diff | annotate
Tue, 12 May 2009 19:30:33 +0200 haftmann transferred code generator preprocessor into separate module file | diff | annotate
Mon, 04 May 2009 14:49:51 +0200 haftmann removed code_name module file | diff | annotate
Fri, 24 Apr 2009 17:45:17 +0200 haftmann observe distinction between Pure/Tools and Tools more closely file | diff | annotate
Wed, 15 Apr 2009 15:52:37 +0200 haftmann code generator bootstrap theory src/Tools/Code_Generator.thy file | diff | annotate
less more (0) tip
isabelle