Zorn and avoid certain
dependencies.
Andrei
--- On Thu, 2/28/13, Lawrence Paulson wrote:
From: Lawrence Paulson
Subject: Re: [isabelle-dev] Zorn's lemma, the well-ordering-theorem, and
extending well-founded relations to (total) well-orders
To: "Christian Sternagel"
Cc: &quo
Hi Alex,
Many thanks for your enthusiasm!
> I'd like to learn about corecursion up-to, which I have not come across so
> far. Are there any good references for this?
A good early account of the up-to techniques at the level of generality we are
interested in is Bartels's
generalized coindu
3, isabelle-dev-requ...@mailbroy.informatik.tu-muenchen.de
wrote:
--
Message: 1
Date: Tue, 6 Aug 2013 03:12:48 -0700 (PDT)
From: Andrei Popescu
To: "isabelle-dev@mailbroy.informatik.tu-muenchen.de"
Subje
Dear Larry,
>> Great news! I hope to see a brief announcement paper illustrating some of
>> the new things that can be done.
A (reminder) example of what you can define with the new package
is your type of hereditarily finite sets.
Best regards,
Andrei
__
> Johannes wrote:
> Theorems about complex numbers are now stated only using Re and Im, the
> Complex
> constructor is not used anymore. It is possible to use primcorec to defined
>the behaviour of a complex-valued function.
>> Makarius wrote:
>> That is indeed very nice. Is that a new invent
.
Andrei
On Tue, 5/13/14, Lawrence Paulson wrote:
Subject: Re: [isabelle-dev] NEWS: avoid the Complex constructor, use the more
natural
To: "Andrei Popescu"
Cc: "isabelle-dev@mailbroy.informatik.tu-muenchen.de"
Date: Tuesday, M
Concerning HyperCTL: I will fix this by Tuesday at 8:00 AM. (Sorry for
delaying this.
I was extremely busy the last weeks, and did not get a chance to pull out the
development version and fix
the problem -- yes, to my shame, I am not using the development version.)
Andrei
On Thursday, Ma
jEdit seems
like a
corridor full of smart people who keep offering to help me. I prefer to do
proofs with my office
door closed.
Andrei
On Thursday, May 15, 2014 11:13 PM, Makarius wrote:
On Thu, 15 May 2014, Andrei Popescu wrote:
> Concerning HyperCTL: I will fix this by Tuesday at
ple"
experience anyway. :-)
I also appreciate your efforts to keep the old army hero alive with Isabelle.
Andrei
On Friday, May 16, 2014 10:57 AM, Makarius wrote:
On Thu, 15 May 2014, Andrei Popescu wrote:
> Proof General is a silent proof partner who gives me a lot
Hi Makarius,
>> (1) Its definition looks terrific:
>> datatype_new (set: 'a) list (map: map rel: list_all2) =
>> =: Nil (defaults tl: "[]") ("[]")
>> | Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
By all "means" terrific. :-)
>From Merriam-Webster dictionary, terrific can mean:
1:
Makarius wrote:
>> Can you explain the squiggle =: above? I did not find it in the manual
>> nor in the sources so far. It seems to be special to main HOL datatypes.
I had not even noticed that weird-looking combination of symbols. :-)
Now I see that what it does is indicate for Nil that
>> datatype_new (set: 'a) list (map: map rel: list_all2) =
>> =: Nil (defaults tl: "[]") ("[]")
>> | Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
>> Can you explain the squiggle =: above? I did not find it in the manual
>> nor in the sources so far. It seems to be special to main HOL dat
I have a comment followed by a suggestion.
Three years ago when I introduced the concept of BNF, I initially called it
"enriched type constructor".
Then people suggested that this name is too unspecific and I came up with "BNF"
("bounded natural functor"),
which summarizes the main compon
Dear Larry, dear all,
>> 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.
Sorry for my late reply. I agree it makes sense to move such basic operators
(and facts) into Main. The Ordinals an
14 matches
Mail list logo
