[isabelle-dev] Number_Theory in ROOT
Lawrence Paulson
lp15 at cam.ac.uk
Wed Jan 29 15:15:28 CET 2014
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"
More information about the isabelle-dev
mailing list