On Fri, 21 Jan 2011, Florian Haftmann wrote:
By chance I discovered that the Isar Implementation Manual in the
release candidate is outdated and does not build from source.
OK, see http://isabelle.in.tum.de/repos/isabelle-release/rev/55b16bd82142
I am still confused why isatest fails due to a
On Fri, 2011-01-21 at 07:27 -0800, Brian Huffman wrote:
> On Fri, Jan 21, 2011 at 7:03 AM, Tjark Weber wrote:
> > Of course, this doesn't work for lemmas that involve separate sorts.
>
> I'm not sure if this is what you have in mind, but in HOLCF there is a
> continuity predicate
>
> cont :: ('a
On Fri, Jan 21, 2011 at 7:03 AM, Tjark Weber wrote:
> On Fri, 2011-01-21 at 15:27 +0100, Tobias Nipkow wrote:
>> One issue can be that if some sort involves multiple type classes, the
>> corresponding class may not have been defined. That is the one advantage
>> of sorts: you can create conjunctio
By chance I discovered that the Isar Implementation Manual in the
release candidate is outdated and does not build from source.
My personal situation does not allow me to correct this personally, but
it should be easily accomplished.
All the best,
Florian
--
Home:
http://www.in.tum.de/
On Fri, 2011-01-21 at 15:27 +0100, Tobias Nipkow wrote:
> One issue can be that if some sort involves multiple type classes, the
> corresponding class may not have been defined. That is the one advantage
> of sorts: you can create conjunctions/intersection of type classes on
> the fly.
If there is
One issue can be that if some sort involves multiple type classes, the
corresponding class may not have been defined. That is the one advantage
of sorts: you can create conjunctions/intersection of type classes on
the fly.
Tobias
Tjark Weber schrieb:
> Hi,
>
> I noticed that numerous lemmas in H
Hi,
I noticed that numerous lemmas in HOL that refer to class constants are
stated at the top level (using implicit or explicit sort annotations),
rather than in the corresponding class context (see, for instance,
Compl_lessThan in HOL/SetInterval.thy). If I am not mistaken, this
means the corres