src/HOL/ROOT

   theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
 
 session "HOL-Number_Theory" in Number_Theory = HOL +
   description {*
     Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
-    Theorem, Wilson's Theorem, Quadratic Reciprocity.
+    Theorem, Wilson's Theorem, some lemmas for 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
+    Gauss
     Number_Theory
   files
     "document/root.tex"
 
 session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL +