src/HOL/Library/Code_Index.thy
2008-09-25 haftmann 2008-09-25 non left-linear equations for nbe
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-08-28 krauss 2008-08-28 more function -> fun
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-06-10 haftmann 2008-06-10 rep_datatype command now takes list of constructors as input arguments
2008-03-17 wenzelm 2008-03-17 avoid rebinding of existing facts;
2008-03-12 haftmann 2008-03-12 yet another useful lemma
2008-02-26 haftmann 2008-02-26 Zero/Suc recursion combinator for type index
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-25 haftmann 2008-01-25 fixed and tuned
2008-01-23 haftmann 2008-01-23 yet another OCaml fix
2008-01-22 haftmann 2008-01-22 fixed OCaml
2008-01-21 haftmann 2008-01-21 tuned code setup
2008-01-15 haftmann 2008-01-15 tuned
2008-01-02 haftmann 2008-01-02 index now a copy of nat rather than int
2007-12-18 haftmann 2007-12-18 switched from PreList to ATP_Linkup
2007-11-29 haftmann 2007-11-29 instance command as rudimentary class target
2007-11-08 haftmann 2007-11-08 duv, mod, int conversion
2007-10-12 haftmann 2007-10-12 added