<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<style type="text/css" style="display:none;"><!-- P {margin-top:0;margin-bottom:0;} --></style>
</head>
<body dir="ltr">
<div id="divtagdefaultwrapper" dir="ltr" style="font-size:12pt; color:rgb(0,0,0); font-family:Calibri,Helvetica,sans-serif,Helvetica,EmojiFont,"Apple Color Emoji","Segoe UI Emoji",NotoColorEmoji,"Segoe UI Symbol","Android Emoji",EmojiSymbols">
<p style="margin-top:0; margin-bottom:0"> Dear Larry, dear all, </p>
<p style="margin-top:0; margin-bottom:0"><br>
</p>
<p style="margin-top:0; margin-bottom:0">>> <span style="font-size:14.666666984558105px">I suggest moving at least the definition of </span>Fpow<span style="font-size:14.666666984558105px"> into Main (</span>it's<span style="font-size:14.666666984558105px"> small,
and fundamental) while creating a new Library entry for my own new material.</span></p>
<p style="margin-top:0; margin-bottom:0"><span style="font-size:14.666666984558105px"><br>
</span></p>
<p style="margin-top:0; margin-bottom:0"><span style="font-size:14.666666984558105px">Sorry for my late reply. I agree it makes sense to move such basic operators (and facts) into Main. The Ordinals and Cardinals development was "destined" to this sort of exports
from the very beginning. </span></p>
<p style="margin-top:0; margin-bottom:0"><span style="font-size:14.666666984558105px"><br>
</span></p>
<p style="margin-top:0; margin-bottom:0"><span style="font-size:14.666666984558105px">Best wishes, </span></p>
<p style="margin-top:0; margin-bottom:0"><span style="font-size:14.666666984558105px"><br>
</span></p>
<p style="margin-top:0; margin-bottom:0"><span style="font-size:14.666666984558105px">Andrei </span></p>
<div style="color:rgb(0,0,0)">
<div class="BodyFragment"><font size="2"><span style="font-size:11pt">
<div class="PlainText"><br>
<br>
----------------------------------------------------------------------<br>
<br>
Message: 1<br>
Date: Wed, 23 Jan 2019 14:33:30 +0000<br>
From: Lawrence Paulson <lp15@cam.ac.uk><br>
To: Jasmin Blanchette <j.c.blanchette@vu.nl><br>
Cc: Traytel Dmitriy <traytel@inf.ethz.ch>, isabelle-dev<br>
<isabelle-dev@in.tum.de><br>
Subject: Re: [isabelle-dev] [Spam] cardinality primitives in<br>
Isabelle/HOL?<br>
Message-ID: <CB1B1CE8-3491-4FCE-8494-6D2E3E68BB94@cam.ac.uk><br>
Content-Type: text/plain; charset=utf-8<br>
<br>
This makes perfect sense to me.<br>
<br>
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.<br>
<br>
Larry<br>
<br>
> On 23 Jan 2019, at 12:48, Blanchette, J.C. <j.c.blanchette@vu.nl> wrote:<br>
> <br>
> Hi Larry,<br>
> <br>
> You wrote:<br>
> <br>
>> The theorem ordIso_iff_ordLeq is proved in BNF_Wellorder_Constructions, so clearly a lot of facts about cardinals are available already in Main.<br>
> <br>
> FYI: As you might already know or deduced from the name convention, the (co)datatype (a.k.a. "BNF") package is based on some cardinality material. When we moved the BNF package into Main, I surgically split the HOL-Cardinals theories into two, moving the
exact dependencies into Main and leaving the rest outside. As a result, it's pretty random what's in Main and what's outside. The alternative -- moving all of HOL-Cardinals into Main -- seemed undesirable because it would slow down building Main quite a bit.<br>
> <br>
> Jasmin<br>
> <br>
<br>
<br>
<br>
</div>
</span></font></div>
</div>
</div>
</body>
</html>