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
On Wed, 29 Jan 2014, Lawrence Paulson wrote:
session HOL-Number_Theory in Number_Theory = HOL +
options [document = false]
theories Number_Theory
As long as there is a global document = false here, it does not matter in
which order which theories are loaded.
The update could be taken as
Hi all,
The meson proof method outputs some annoying messages like
0 inferences so far. Searching to depth 0
3 inferences so far. Searching to depth 5
6 inferences so far. Searching to depth 15
9 inferences so far. Searching to depth 25
12 inferences so far. Searching to depth 35
