Re: [isabelle-dev] Isatest

2012-03-30 Thread Lukas Bulwahn
The webpage on the Isabelle (community) wiki, https://isabelle.in.tum.de/community/Administration_of_the_isatest_facilities, summarizes the agreement of this thread. If anyone wants to add or modify the page, feel free to do so. Lukas On 03/29/2012 09:29 AM, Gerwin Klein wrote: On

Re: [isabelle-dev] Isatest

2012-03-30 Thread Makarius
On Fri, 30 Mar 2012, Lukas Bulwahn wrote: The webpage on the Isabelle (community) wiki, https://isabelle.in.tum.de/community/Administration_of_the_isatest_facilities, summarizes the agreement of this thread. If anyone wants to add or modify the page, feel free to do so. I am still not

Re: [isabelle-dev] Isatest

2012-03-30 Thread Makarius
On Fri, 30 Mar 2012, Lukas Bulwahn wrote: On 03/30/2012 11:24 AM, Makarius wrote: On Fri, 30 Mar 2012, Lukas Bulwahn wrote: The webpage on the Isabelle (community) wiki, https://isabelle.in.tum.de/community/Administration_of_the_isatest_facilities, summarizes the agreement of this thread.

Re: [isabelle-dev] JDK / Mira

2012-03-30 Thread Makarius
This is yet another attempt to get things right, and reasonably simple. * The isatest account takes care to provide reasonable $JAVE_HOME via its shell environment (the same for SCALA_HOME, but that is less critical). This is based on the observation that JAVA_HOME is difficult to

Re: [isabelle-dev] Relations vs. Predicates

2012-03-30 Thread Florian Haftmann
Hi Christian, To come back to the subject, I'm missing iteration of predicates, i.e., what _^^n is on relations but for predicates ('a = 'a = bool). this has been added in http://isabelle.in.tum.de/testboard/Isabelle/rev/69cee87927f0 – you can transfer theorems from the set relations in an