src/HOL/Code_Numeral.thy
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;
Mon, 23 Jul 2012 09:28:03 +0200 haftmann restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
Sun, 01 Apr 2012 16:09:58 +0200 huffman removed Nat_Numeral.thy, moving all theorems elsewhere
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
Mon, 20 Feb 2012 12:37:17 +0100 huffman use qualified constant names instead of suffixes (from Florian Haftmann)
Thu, 29 Dec 2011 10:47:55 +0100 haftmann attribute code_abbrev superseedes code_unfold_post
Wed, 30 Nov 2011 16:27:10 +0100 wenzelm prefer typedef without extra definition and alternative name;
Wed, 07 Sep 2011 09:02:58 -0700 huffman avoid using legacy theorem names
Fri, 01 Oct 2010 14:15:49 +0200 haftmann use module integer for Eval
Fri, 10 Sep 2010 10:21:25 +0200 haftmann Haskell == is infix, not infixl
Fri, 27 Aug 2010 19:34:23 +0200 haftmann renamed class/constant eq to equal; tuned some instantiations
Sat, 24 Jul 2010 18:08:41 +0200 haftmann another refinement chapter in the neverending numeral story
Fri, 23 Jul 2010 10:58:13 +0200 haftmann avoid unreliable Haskell Int type
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;
Wed, 31 Mar 2010 16:44:41 +0200 bulwahn adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
Wed, 10 Mar 2010 15:29:21 +0100 haftmann tuned whitespace
Fri, 05 Feb 2010 14:33:50 +0100 haftmann more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
Fri, 22 Jan 2010 13:38:28 +0100 haftmann code literals: distinguish numeral classes by different entries
Fri, 15 Jan 2010 14:43:00 +0100 berghofe merged
Sun, 10 Jan 2010 18:43:45 +0100 berghofe Adapted to changes in induct method.
Thu, 14 Jan 2010 17:47:38 +0100 haftmann allow individual printing of numerals during code serialization
Wed, 13 Jan 2010 08:56:15 +0100 haftmann some syntax setup for Scala
Thu, 29 Oct 2009 22:13:09 +0100 haftmann moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
Thu, 29 Oct 2009 11:41:36 +0100 haftmann moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
Wed, 28 Oct 2009 19:09:47 +0100 haftmann moved theory Divides after theory Nat_Numeral; tuned some proof texts
less more (0) -60 tip