src/HOL/Code_Numeral.thy
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
Tue, 14 Jul 2009 16:27:32 +0200 haftmann prefer code_inline over code_unfold; use code_unfold_post where appropriate
Tue, 14 Jul 2009 10:54:04 +0200 haftmann code attributes use common underscore convention
Tue, 02 Jun 2009 15:53:05 +0200 haftmann OCaml builtin intergers are elusive; avoid
Wed, 27 May 2009 22:11:05 +0200 haftmann added lemma about 0 - 1
Tue, 19 May 2009 16:54:55 +0200 haftmann String.literal replaces message_string, code_numeral replaces (code_)index
less more (0) tip