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
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
