src/HOL/IsaMakefile

   Enum.thy \
   Groebner_Basis.thy \
   Hilbert_Choice.thy \
   Int.thy \
   Lazy_Sequence.thy \
+  Lifting.thy \
   List.thy \
   Main.thy \
   Map.thy \
   Nat_Transfer.thy \
   New_DSequence.thy \

   $(SRC)/Provers/Arith/extract_common_term.ML \
   Tools/choice_specification.ML \
   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 \
   Tools/Nitpick/kodkod.ML \
   Tools/Nitpick/kodkod_sat.ML \

 HOL-Isar_Examples: HOL $(LOG)/HOL-Isar_Examples.gz
 
 $(LOG)/HOL-Isar_Examples.gz: $(OUT)/HOL Isar_Examples/Basic_Logic.thy	\
   Isar_Examples/Cantor.thy Isar_Examples/Drinker.thy			\
   Isar_Examples/Expr_Compiler.thy Isar_Examples/Fibonacci.thy		\
-  Isar_Examples/Group.thy Isar_Examples/Hoare.thy			\
+  Isar_Examples/Group.thy Isar_Examples/Group_Context.thy		\
+  Isar_Examples/Group_Notepad.thy Isar_Examples/Hoare.thy		\
   Isar_Examples/Hoare_Ex.thy Isar_Examples/Knaster_Tarski.thy		\
   Isar_Examples/Mutilated_Checkerboard.thy				\
   Isar_Examples/Nested_Datatype.thy Isar_Examples/Peirce.thy		\
   Isar_Examples/Puzzle.thy Isar_Examples/Summation.thy			\
   Isar_Examples/ROOT.ML Isar_Examples/document/proof.sty		\

 $(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL				\
   Quotient_Examples/DList.thy \
   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
 
 
 ## HOL-Predicate_Compile_Examples