Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
include Int_Pow into Quotient_Examples; add end of the theory
authorkuncar
Tue, 17 Sep 2013 14:10:33 +0200
changeset 53682 1b55aeda0e46
parent 53681 7e80b558c751
child 53683 e6adad558def
include Int_Pow into Quotient_Examples; add end of the theory
src/HOL/Quotient_Examples/Int_Pow.thy file | annotate | diff | comparison | revisions
src/HOL/ROOT file | annotate | diff | comparison | revisions 
--- 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
--- 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]
isabelle