1.1 --- a/src/HOL/Quotient_Examples/Int_Pow.thy	Tue Sep 17 13:40:44 2013 +0200
     1.2 +++ b/src/HOL/Quotient_Examples/Int_Pow.thy	Tue Sep 17 14:10:33 2013 +0200
     1.3 @@ -144,3 +144,5 @@
     1.4  lifting_forget int.lifting
     1.5  
     1.6  end
     1.7 +
     1.8 +end

     2.1 --- a/src/HOL/ROOT	Tue Sep 17 13:40:44 2013 +0200
     2.2 +++ b/src/HOL/ROOT	Tue Sep 17 14:10:33 2013 +0200
     2.3 @@ -914,6 +914,7 @@
     2.4      Lift_Fun
     2.5      Quotient_Rat
     2.6      Lift_DList
     2.7 +    Int_Pow
     2.8  
     2.9  session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
    2.10    options [document = false]