src/HOL/Library/Code_Integer.thy
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