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
> [email protected]
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
