src/HOL/ROOT
changeset 55730 97ff9276e12d
parent 55663 12448c179851
child 55973 471a71017cfc
--- a/src/HOL/ROOT	Mon Feb 24 22:41:08 2014 +0100
+++ b/src/HOL/ROOT	Mon Feb 24 23:17:55 2014 +0000
@@ -173,7 +173,7 @@
 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]
@@ -183,6 +183,7 @@
     "~~/src/HOL/Algebra/FiniteProduct"
   theories
     Pocklington
+    Gauss
     Number_Theory
   files
     "document/root.tex"