isabelle: File revisions

src/HOL/Tools/Lifting/lifting_def_code_dt.ML

Sun, 07 Jun 2015 20:03:40 +0200	wenzelm	tuned signature;	file \| diff \| annotate
Sun, 03 May 2015 14:35:48 +0200	wenzelm	make SML/NJ more happy;	file \| diff \| annotate
Sat, 02 May 2015 13:58:06 +0200	kuncar	handle error messages also in after_qed	file \| diff \| annotate
Sat, 02 May 2015 13:58:06 +0200	kuncar	reorder some steps in the construction to support mutual datatypes	file \| diff \| annotate
Sat, 02 May 2015 13:58:06 +0200	kuncar	more readable error message if some types do not correspond to sort constraints of the datatype	file \| diff \| annotate
Sat, 02 May 2015 13:58:06 +0200	kuncar	better precomputing	file \| diff \| annotate
Sat, 02 May 2015 13:58:06 +0200	kuncar	equivalence in code_dt data structure must respect both rty and qty	file \| diff \| annotate
Sat, 02 May 2015 13:58:06 +0200	kuncar	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	file \| diff \| annotate
Mon, 13 Apr 2015 15:27:34 +0200	kuncar	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	file \| diff \| annotate
Fri, 05 Dec 2014 14:14:36 +0100	kuncar	Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype	file \| diff \| annotate

isabelle