[isabelle-dev] Number_Theory in ROOT

[Tobias Nipkow]

On 29/01/2014 15:15, Lawrence Paulson wrote:
> I’m puzzled about the inconsistency between the treatment of the new and old number theory libraries in the file ROOT.
> 
> The old one is as I would expect, with a description and the loading of some antecedent theories with document output suppressed. The new one basically looks like a stub. Is this just an oversight?
> 
> Larry
> 
> 
> session "HOL-Number_Theory" in Number_Theory = HOL +
>   options [document = false]
>   theories Number_Theory

I suspect Number_Theory loads everything automatically.

Tobias

> session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL +
>   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/Infinite_Set"
>     "~~/src/HOL/Library/Permutation"
>   theories
>     Fib
>     Factorization
>     Chinese
>     WilsonRuss
>     WilsonBij
>     Quadratic_Reciprocity
>     Primes
>     Pocklington
>   files "document/root.tex"
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>