src/HOL/Library/Code_Integer.thy
2012-07-23 haftmann 2012-07-23 restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
2012-06-05 haftmann 2012-06-05 prefer sys.error over plain error in Scala to avoid deprecation warning
2012-03-30 huffman 2012-03-30 removed redundant nat-specific copies of theorems
2012-03-26 huffman 2012-03-26 code lemma for function 'nat' that doesn't go into an infinite loop (fixes problem with non-terminating HOL-Proofs-Lambda)
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2010-09-10 haftmann 2010-09-10 Haskell == is infix, not infixl
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-08-26 haftmann 2010-08-26 prevent line breaks after Scala symbolic operators
2010-07-28 haftmann 2010-07-28 may use `int` in Isabelle runtime environment
2010-07-26 haftmann 2010-07-26 added Code_Natural.thy
2010-07-24 haftmann 2010-07-24 another refinement chapter in the neverending numeral story
2010-07-23 haftmann 2010-07-23 avoid unreliable Haskell Int type
2010-01-22 haftmann 2010-01-22 code literals: distinguish numeral classes by different entries
2010-01-14 haftmann 2010-01-14 added Scala setup
2009-09-23 haftmann 2009-09-23 Code_Eval(uation)
2009-06-02 haftmann 2009-06-02 OCaml builtin intergers are elusive; avoid
2009-05-19 haftmann 2009-05-19 String.literal replaces message_string, code_numeral replaces (code_)index
2009-05-19 haftmann 2009-05-19 moved Code_Index, Random and Quickcheck before Main
2009-05-18 haftmann 2009-05-18 added Code_Index.int_of operation
2009-03-23 haftmann 2009-03-23 Main is (Complex_Main) base entry point in library theories
2009-02-16 haftmann 2009-02-16 added pdivmod on int (for code generation)
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-09-25 haftmann 2008-09-25 discontinued special treatment of op = vs. eq_class.eq
2008-09-16 haftmann 2008-09-16 evaluation using code generator
2008-07-07 haftmann 2008-07-07 absolute imports of HOL/*.thy theories
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2008-03-28 haftmann 2008-03-28 accomodated to sledgehammer theory dependency requirement
2008-02-17 huffman 2008-02-17 New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
2008-01-29 haftmann 2008-01-29 treating division by zero properly
2008-01-21 haftmann 2008-01-21 tuned code setup
2008-01-15 haftmann 2008-01-15 joined theories IntDef, Numeral, IntArith to theory Int
2008-01-02 haftmann 2008-01-02 index now a copy of nat rather than int
2007-10-12 haftmann 2007-10-12 added