src/HOL/ROOT
changeset 55321 eadea363deb6
parent 55240 efc4c0e0e14a
child 55370 e6be866b5f5b
     1.1 --- a/src/HOL/ROOT	Tue Feb 04 21:01:35 2014 +0100
     1.2 +++ b/src/HOL/ROOT	Tue Feb 04 21:28:38 2014 +0000
     1.3 @@ -171,8 +171,19 @@
     1.4    theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
     1.5  
     1.6  session "HOL-Number_Theory" in Number_Theory = HOL +
     1.7 -  options [document = false]
     1.8 -  theories Number_Theory
     1.9 +  description {*
    1.10 +    Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
    1.11 +    Theorem, Wilson's Theorem, Quadratic Reciprocity.
    1.12 +  *}
    1.13 +  options [document_graph]
    1.14 +  theories [document = false]
    1.15 +    "~~/src/HOL/Library/FuncSet"
    1.16 +    "~~/src/HOL/Library/Multiset"
    1.17 +    "~~/src/HOL/Algebra/Ring"
    1.18 +    "~~/src/HOL/Algebra/FiniteProduct"
    1.19 +  theories
    1.20 +    Pocklington
    1.21 +    Number_Theory
    1.22  
    1.23  session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL +
    1.24    description {*