Re: [isabelle-dev] [release] IsarImplementation

2011-01-21 Thread Makarius
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

Re: [isabelle-dev] Sort Annotation vs. Class Context for Lemmas

2011-01-21 Thread Tjark Weber
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

Re: [isabelle-dev] Sort Annotation vs. Class Context for Lemmas

2011-01-21 Thread Brian Huffman
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

[isabelle-dev] [release] IsarImplementation

2011-01-21 Thread Florian Haftmann
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/

Re: [isabelle-dev] Sort Annotation vs. Class Context for Lemmas

2011-01-21 Thread Tjark Weber
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

Re: [isabelle-dev] Sort Annotation vs. Class Context for Lemmas

2011-01-21 Thread Tobias Nipkow
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

[isabelle-dev] Sort Annotation vs. Class Context for Lemmas

2011-01-21 Thread Tjark Weber
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