# HG changeset patch
# User kuncar
# Date 1379419833 -7200
# Node ID 1b55aeda0e468f9e152d84eec0d2536f03b80536
# Parent  7e80b558c7513b57670ddf9f7305ef6a138c0003
include Int_Pow into Quotient_Examples; add end of the theory

diff -r 7e80b558c751 -r 1b55aeda0e46 src/HOL/Quotient_Examples/Int_Pow.thy
--- a/src/HOL/Quotient_Examples/Int_Pow.thy	Tue Sep 17 13:40:44 2013 +0200
+++ b/src/HOL/Quotient_Examples/Int_Pow.thy	Tue Sep 17 14:10:33 2013 +0200
@@ -144,3 +144,5 @@
 lifting_forget int.lifting
 
 end
+
+end
diff -r 7e80b558c751 -r 1b55aeda0e46 src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Sep 17 13:40:44 2013 +0200
+++ b/src/HOL/ROOT	Tue Sep 17 14:10:33 2013 +0200
@@ -914,6 +914,7 @@
     Lift_Fun
     Quotient_Rat
     Lift_DList
+    Int_Pow
 
 session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
   options [document = false]