diff -r 432b29a96f61 -r dac11ab96277 src/HOL/IsaMakefile --- 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