Re: [isabelle-dev] Remaining uses of Proof General?

Makarius > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- Cezary Kaliszyk, University of Innsbruck, http://cl

Re: [isabelle-dev] New HOL/Import

On Thu, Mar 29, 2012 at 8:04 PM, Makarius wrote: > Wow, I am impressed by the brevity of it.  You should mention the secret > http://cl-informatik.uibk.ac.at/~cek/proofs which is a bzip stream to be > uncompressed, before it can be used with import_file in the example. That's the preprocessed pro

[isabelle-dev] New HOL/Import

ac.at/~cek/import.tgz Regards, Cezary -- Cezary Kaliszyk, University of Innsbruck, http://cl-informatik.uibk.ac.at/~cek/ ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] [isabelle] Status of HOL/Import

Hi Florian, On Sun, Mar 04, 2012 at 10:15:38AM +0100, Florian Haftmann wrote: > I've been working on the Importer stuff, not very deeply, but separating > HOL4 and HOL Light contents, stripping generic parts of any name > reference to HOL4, etc. [...] Great! > There could be done a lot more on t

Re: [isabelle-dev] Quotient example with partiality?

Hi Florian, All, 2011/11/29 Florian Haftmann : > I'm asking myself the question how one would define rational numbers > using the quotient package.  The key issue is that the equivalence > relation here is partial, ruling out denominators of value zero.  In the > Isabelle reference manual I can fi

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

On Fri, Aug 26, 2011 at 5:45 AM, Florian Haftmann < florian.haftm...@informatik.tu-muenchen.de> wrote: > > [...] According to my knowledge, the following session produce > problems: [...] > HOL-Quotient_Examples FAILED > Please propagare the isabelle changeset: http://isabelle.in.tum.de/repos/isab

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

On Thu, Aug 18, 2011 at 3:49 AM, Florian Haftmann < florian.haftm...@informatik.tu-muenchen.de> wrote: > [...] So, the best way now is > to continue eliminating set-pred mixture (also in the AFP of course!) > and discover problems in packages – I'm a little concerned about > quotient since this ha

Re: [isabelle-dev] Testing HOL/Import

On Wed, Jul 20, 2011 at 11:33 AM, Alexander Krauss wrote: > Now my question is: What do we actually know when HOL-Generate-HOLLight > completes without error? Should the generated file be compared with the > version in the repository and should the test fail when they are not > identical? Are ther

Re: [isabelle-dev] [isabelle] Status of HOL/Import

On Wed, Jul 13, 2011 at 4:51 PM, Alexander Krauss wrote: > On 07/12/2011 11:15 PM, Florian Haftmann wrote: > I just tried to redo this to see how it works > $ svn checkout http://hol-light.googlecode.com/svn/trunk/ hol_light > $ cd hol_light/Proofrecording/hol_light > $ make > and it failed with >

Re: [isabelle-dev] [isabelle] Status of HOL/Import

Hi Florian, On Wed, Jul 13, 2011 at 6:15 AM, Florian Haftmann wrote: > Of course there is a lot one could clean up.  In my eyes there are some > issues which prevent an understanding of HOL-Import »in the large«, and > maybe your experience could answer the following questions: > > a) HOL-Import

[isabelle-dev] Workshop on Mathematical Wikis at ITP 2011 (Nijmegen, NL, August 27; abstract submission May 30)

: June 23rd, 2011 * Camera ready versions due: July 11th, 2011 * Workshop: August 27th, 2011 PROGRAM COMMITTEE * Jesse Alama * David Aspinall * Joe Corneli * Cezary Kaliszyk * Fairouz Kamareddine * Michael Kohlhase * Markus Krötzsch * Christoph Lange (co-chair) * Lionel Mamane

[isabelle-dev] Document preparation failure

can rebuild the HOL-Main > image (assuming it works!) > > - Brian > ___ > Isabelle-dev mailing list > Isabelle-dev at mailbroy.informatik.tu-muenchen.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >