--- a/src/HOL/IsaMakefile Tue Apr 03 15:15:00 2012 +0200
+++ b/src/HOL/IsaMakefile Tue Apr 03 20:56:32 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 \
@@ -1036,7 +1041,8 @@
$(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 \
@@ -1495,7 +1501,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