src/HOL/IsaMakefile
changeset 47308 9caab698dbe4
parent 47267 4c7548e7df86
child 47310 610d9c212376
--- a/src/HOL/IsaMakefile	Tue Apr 03 14:09:37 2012 +0200
+++ b/src/HOL/IsaMakefile	Tue Apr 03 16:26:48 2012 +0200
@@ -281,6 +281,7 @@
   Hilbert_Choice.thy \
   Int.thy \
   Lazy_Sequence.thy \
+  Lifting.thy \
   List.thy \
   Main.thy \
   Map.thy \
@@ -315,6 +316,10 @@
   Tools/code_evaluation.ML \
   Tools/groebner.ML \
   Tools/int_arith.ML \
+  Tools/Lifting/lifting_def.ML \
+  Tools/Lifting/lifting_info.ML \
+  Tools/Lifting/lifting_term.ML \
+  Tools/Lifting/lifting_setup.ML \
   Tools/list_code.ML \
   Tools/list_to_set_comprehension.ML \
   Tools/nat_numeral_simprocs.ML \
@@ -1495,7 +1500,7 @@
   Quotient_Examples/FSet.thy \
   Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy \
   Quotient_Examples/Lift_Set.thy Quotient_Examples/Lift_RBT.thy \
-  Quotient_Examples/Lift_Fun.thy 
+  Quotient_Examples/Lift_Fun.thy Quotient_Examples/Lift_DList.thy
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples