Go right ahead. I had no idea this was even still used.
Larry
On 29 Jan 2014, at 23:33, Jasmin Christian Blanchette
wrote:
> 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
>
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
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
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 su
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 th
