src/HOL/Code_Numeral.thy
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;
less more (0) -50 -30 tip