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

___ 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-informatik.uibk.ac.at/~cek

Re: [isabelle-dev] New HOL/Import

On Thu, Mar 29, 2012 at 8:04 PM, Makarius makar...@sketis.net 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

[isabelle-dev] New HOL/Import

/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 the

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 has

Re: [isabelle-dev] Testing HOL/Import

On Wed, Jul 20, 2011 at 11:33 AM, Alexander Krauss kra...@in.tum.de 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

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

On Wed, Jul 13, 2011 at 4:51 PM, Alexander Krauss kra...@in.tum.de 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

[isabelle-dev] Document preparation failure

(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 -- Cezary Kaliszyk kaliszyk at in.tum.de Nominal Methods Group