src/HOL/Code_Numeral.thy
Sat, 30 Mar 2019 15:37:22 +0100 haftmann irrelevant
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;
Fri, 22 Mar 2019 19:18:08 +0000 haftmann improved code equations taken over from AFP
Sun, 10 Mar 2019 15:16:45 +0000 haftmann migrated from Nums to Zarith as library for OCaml integer arithmetic
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Tue, 24 Apr 2018 14:17:58 +0000 haftmann proper datatype for 8-bit characters
Fri, 20 Apr 2018 07:36:58 +0000 haftmann algebraic embeddings for bit operations
Tue, 20 Mar 2018 09:27:39 +0000 haftmann generalized
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Wed, 03 Jan 2018 11:06:13 +0100 blanchet kill old size infrastructure
Fri, 20 Oct 2017 07:46:10 +0200 haftmann added lemmas and tuned proofs
Mon, 09 Oct 2017 19:10:51 +0200 haftmann clarified parity
Mon, 09 Oct 2017 19:10:49 +0200 haftmann clarified uniqueness criterion for euclidean rings
Mon, 09 Oct 2017 19:10:47 +0200 haftmann tuned imports
Sun, 08 Oct 2017 22:28:22 +0200 haftmann euclidean rings need no normalization
Sun, 08 Oct 2017 22:28:22 +0200 haftmann one uniform type class for parity structures
Sun, 08 Oct 2017 22:28:21 +0200 haftmann abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
Sun, 08 Oct 2017 22:28:20 +0200 haftmann avoid fact name clashes
Sat, 24 Jun 2017 09:17:35 +0200 haftmann more direct construction of integer_of_num;
Mon, 06 Feb 2017 20:56:38 +0100 haftmann computation preprocessing rules to allow literals as input for computations
Mon, 09 Jan 2017 18:53:06 +0100 haftmann slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization
Sat, 17 Dec 2016 15:22:14 +0100 haftmann more fine-grained type class hierarchy for div and mod
Sun, 16 Oct 2016 09:31:06 +0200 haftmann eliminated irregular aliasses
Sun, 16 Oct 2016 09:31:04 +0200 haftmann transfer rules for divides relation on integer and natural
Wed, 12 Oct 2016 21:48:53 +0200 haftmann transfer lifting rule for numeral
Mon, 26 Sep 2016 07:56:54 +0200 haftmann syntactic type class for operation mod named after mod;
Sun, 29 May 2016 14:43:17 +0200 haftmann do not export abstract constructors in code_reflect
Fri, 18 Dec 2015 14:23:11 +0100 Andreas Lochbihler add serialisation for abs on integer to target language operation
Sun, 27 Sep 2015 10:11:15 +0200 haftmann monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
Sun, 27 Sep 2015 10:11:14 +0200 haftmann more selective preprocessing allows bare "numeral" occurences to be retained as real function in generated code
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Sat, 08 Aug 2015 10:51:33 +0200 haftmann direct bootstrap of integer division from natural division
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Tue, 23 Jun 2015 16:55:28 +0100 paulson Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
Mon, 01 Jun 2015 18:59:21 +0200 haftmann separate class for division operator, with particular syntax added in more specific classes
Mon, 23 Mar 2015 19:05:14 +0100 haftmann distributivity of partial minus establishes desired properties of dvd in semirings
Fri, 06 Feb 2015 17:57:03 +0100 haftmann default abstypes and default abstract equations make technical (no_code) annotation superfluous
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Thu, 18 Sep 2014 18:48:54 +0200 haftmann always annotate potentially polymorphic Haskell numerals
Thu, 18 Sep 2014 18:48:04 +0200 haftmann tuned
Fri, 19 Sep 2014 13:27:04 +0200 blanchet keep obsolete interpretations in Main, to avoid merge trouble
Thu, 18 Sep 2014 16:57:10 +0200 blanchet reintroduced an instantiation of 'size' for 'numerals'
Thu, 18 Sep 2014 16:47:40 +0200 blanchet moved old 'size' generator together with 'old_datatype'
Thu, 11 Sep 2014 18:54:36 +0200 blanchet renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Sun, 04 May 2014 18:14:58 +0200 blanchet renamed 'xxx_size' to 'size_xxx' for old datatype package
Thu, 06 Mar 2014 15:40:33 +0100 blanchet renamed 'fun_rel' to 'rel_fun'
Tue, 25 Feb 2014 19:07:14 +0100 kuncar unregister lifting setup following the best practice of Lifting
Fri, 21 Feb 2014 00:09:56 +0100 blanchet adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
Wed, 12 Feb 2014 10:59:25 +0100 Andreas Lochbihler merged
Wed, 12 Feb 2014 09:06:04 +0100 Andreas Lochbihler make integer_of_char and char_of_integer work with NBE and code_simp
Wed, 12 Feb 2014 08:35:57 +0100 blanchet adapted theories to 'xxx_case' to 'case_xxx'
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed '{prod,sum,bool,unit}_case' to 'case_...'
Tue, 19 Nov 2013 10:05:53 +0100 haftmann eliminiated neg_numeral in favour of - (numeral _)
Sun, 18 Aug 2013 15:29:50 +0200 haftmann execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
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
Fri, 08 Mar 2013 13:21:06 +0100 kuncar patch Isabelle ditribution to conform to changes regarding the parametricity
Fri, 15 Feb 2013 08:31:31 +0100 haftmann two target language numeral types: integer and natural, as replacement for code_numeral;
Fri, 19 Oct 2012 15:12:52 +0200 webertj Renamed {left,right}_distrib to distrib_{right,left}.
Fri, 12 Oct 2012 18:58:20 +0200 wenzelm discontinued obsolete typedef (open) syntax;
less more (0) -60 tip