Isabelle/20bc1d26c932 now provides an updated polyml-test-a444f281ccec
(active by default).
It performs slightly better than the previous test version -- I have
also removed old workarounds for integer arithmetic in
Isabelle/4591221824f6.
It is important to check that obsolete entries in
On 23/01/2019 21:08, Makarius wrote:
On 23/01/2019 12:05, David Matthews wrote:
I've had a look at this under Windows and the problem seems to be with
calls to IntInf.divMod from generated code, not from IntInf.pow. The
underlying RTS call used by IntInf.quotRem has changed in the 32-in-64
On 23/01/2019 12:05, David Matthews wrote:
>
> I've had a look at this under Windows and the problem seems to be with
> calls to IntInf.divMod from generated code, not from IntInf.pow. The
> underlying RTS call used by IntInf.quotRem has changed in the 32-in-64
> version. It previously returned
On 23/01/2019 14:14, Bertram Felgenhauer wrote:
> Makarius wrote:
>> On 22/01/2019 12:31, Bertram Felgenhauer wrote:
>>> Makarius wrote:
So this is the right time for further testing of applications:
Isabelle2018 should work as well, but I have not done any testing beyond
"isabelle
This makes perfect sense to me.
I suggest moving at least the definition of Fpow into Main (it’s small, and
fundamental) while creating a new Library entry for my own new material.
Larry
> On 23 Jan 2019, at 12:48, Blanchette, J.C. wrote:
>
> Hi Larry,
>
> You wrote:
>
>> The theorem
Makarius wrote:
> On 22/01/2019 12:31, Bertram Felgenhauer wrote:
> > Makarius wrote:
> >> So this is the right time for further testing of applications:
> >> Isabelle2018 should work as well, but I have not done any testing beyond
> >> "isabelle build -g main" -- Isabelle development only moves
Hi Larry,
You wrote:
> The theorem ordIso_iff_ordLeq is proved in BNF_Wellorder_Constructions, so
> clearly a lot of facts about cardinals are available already in Main.
FYI: As you might already know or deduced from the name convention, the
(co)datatype (a.k.a. "BNF") package is based on
The question of dependency is tricky. I tried deleting the reference to
HOL-Cardinals.Cardinals and found that most of the elementary results were
easily provable using other library facts. But then there was this:
lemma lepoll_trans1 [trans]: "⟦A ≈ B; B ≲ C⟧ ⟹ A ≲ C"
by (meson card_of_ordLeq
On 22/01/2019 23:01, Makarius wrote:
On 22/01/2019 23:08, Fabian Immler wrote:
On 1/22/2019 4:00 PM, Fabian Immler wrote:
On 1/22/2019 2:28 PM, Makarius wrote:
On 22/01/2019 20:05, Fabian Immler wrote:
These numbers look quite extreme:
The slowdown in polyml-5.7.1-8 is about a factor of 2-3
Hi Larry,
if you want to put the definitions and the basic properties in Main, then
Fun.thy would probably be the place. But then I would argue that the syntax
should be hidden, as users might want to use these symbols for something else.
For the advanced material, do you need some theorems
> But ocamlfind semms not to provide a subcommand to invoke the
> interactive OCaml toplevel. What am I missing?
The other way round. "ocamlfind" hooks into the toplevel.
$ isabelle ocaml_opam config exec ocaml
OCaml version 4.05.0
# #use "topfind";;
- : unit = ()
Findlib has been
11 matches
Mail list logo