--- a/src/HOL/ROOT Tue Feb 04 21:01:35 2014 +0100
+++ b/src/HOL/ROOT Tue Feb 04 21:28:38 2014 +0000
@@ -171,8 +171,19 @@
theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
session "HOL-Number_Theory" in Number_Theory = HOL +
- options [document = false]
- theories Number_Theory
+ description {*
+ Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
+ Theorem, Wilson's Theorem, Quadratic Reciprocity.
+ *}
+ options [document_graph]
+ theories [document = false]
+ "~~/src/HOL/Library/FuncSet"
+ "~~/src/HOL/Library/Multiset"
+ "~~/src/HOL/Algebra/Ring"
+ "~~/src/HOL/Algebra/FiniteProduct"
+ theories
+ Pocklington
+ Number_Theory
session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL +
description {*