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

2014-12-05 kuncar [Fri, 05 Dec 2014 14:14:36 +0100] rev 60229
Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
src/HOL/Lifting.thy src/HOL/Lifting_Set.thy src/HOL/Tools/Lifting/lifting_def.ML src/HOL/Tools/Lifting/lifting_def_code_dt.ML src/HOL/Tools/Lifting/lifting_util.ML src/HOL/Transfer.thy

2014-12-05 kuncar [Fri, 05 Dec 2014 14:14:36 +0100] rev 60228
tuned proof; forget the transfer rule for size_fset
src/HOL/Library/FSet.thy

2014-12-05 kuncar [Fri, 05 Dec 2014 14:14:36 +0100] rev 60227
return also which code equation was used; tuned
src/HOL/Tools/Lifting/lifting_def.ML

2014-12-05 kuncar [Fri, 05 Dec 2014 14:14:36 +0100] rev 60226
publish lifting_forget and lifting_udpate interface
src/HOL/Tools/Lifting/lifting_setup.ML

2014-12-05 kuncar [Fri, 05 Dec 2014 14:14:36 +0100] rev 60225
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
src/HOL/Tools/Lifting/lifting_def.ML src/HOL/Tools/Lifting/lifting_setup.ML src/HOL/Tools/Quotient/quotient_type.ML

2014-11-18 kuncar [Tue, 18 Nov 2014 16:19:57 +0100] rev 60224
export the result of lifting_def
src/HOL/Tools/Lifting/lifting_def.ML

2014-11-18 kuncar [Tue, 18 Nov 2014 16:19:57 +0100] rev 60223
useful function
src/HOL/Tools/Lifting/lifting_util.ML

2014-11-18 kuncar [Tue, 18 Nov 2014 16:19:57 +0100] rev 60222
parametrize liting of terms by quotients
src/HOL/Tools/Lifting/lifting_term.ML