2015-05-03 wenzelm [Sun, 03 May 2015 14:35:48 +0200] rev 60239
make SML/NJ more happy;
src/HOL/Tools/Lifting/lifting_def.ML src/HOL/Tools/Lifting/lifting_def_code_dt.ML src/HOL/Tools/Lifting/lifting_setup.ML src/HOL/Tools/Lifting/lifting_term.ML

2015-05-03 wenzelm [Sun, 03 May 2015 14:12:10 +0200] rev 60238
tuned message;
src/Tools/jEdit/src/token_markup.scala

2015-05-02 kuncar [Sat, 02 May 2015 13:58:06 +0200] rev 60237
add testing file for code_dt extension of lifting
src/HOL/Quotient_Examples/Lifting_Code_Dt_Test.thy src/HOL/ROOT

2015-05-02 kuncar [Sat, 02 May 2015 13:58:06 +0200] rev 60236
handle error messages also in after_qed
src/HOL/Tools/Lifting/lifting_def_code_dt.ML

2015-05-02 kuncar [Sat, 02 May 2015 13:58:06 +0200] rev 60235
reorder some steps in the construction to support mutual datatypes
src/HOL/Tools/Lifting/lifting_def_code_dt.ML src/HOL/Tools/Lifting/lifting_info.ML

2015-05-02 kuncar [Sat, 02 May 2015 13:58:06 +0200] rev 60234
more readable error message if some types do not correspond to sort constraints of the datatype
src/HOL/Tools/Lifting/lifting_def_code_dt.ML

2015-05-02 kuncar [Sat, 02 May 2015 13:58:06 +0200] rev 60233
better precomputing
src/HOL/Tools/Lifting/lifting_def_code_dt.ML

2015-05-02 kuncar [Sat, 02 May 2015 13:58:06 +0200] rev 60232
equivalence in code_dt data structure must respect both rty and qty
src/HOL/Tools/Lifting/lifting_def_code_dt.ML

2015-05-02 kuncar [Sat, 02 May 2015 13:58:06 +0200] rev 60231
don't use the human-readable version of the rsp thm as a goal in the ML interface (there is no formal definition of its statement); make tactics more robust wrt. predicates in predicators; tuned
src/HOL/Tools/Lifting/lifting_def.ML src/HOL/Tools/Lifting/lifting_def_code_dt.ML src/HOL/Tools/Lifting/lifting_setup.ML

2015-04-13 kuncar [Mon, 13 Apr 2015 15:27:34 +0200] rev 60230
go back to the complicated code equation registration (because of type classes) that was lost in 922586b1bc87; make it even more hackish to get which code equation was used
src/HOL/Tools/Lifting/lifting_def.ML src/HOL/Tools/Lifting/lifting_def_code_dt.ML