src/HOL/Library/Code_Index.thy
2009-02-06 haftmann 2009-02-06 session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
2009-02-06 haftmann 2009-02-06 mandatory prefix for index conversion operations
2008-10-29 haftmann 2008-10-29 explicit check for pattern discipline before code translation
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
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