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
but I would
suggest waiting a week or two for the new import and trying to get
the maps correct there.
Ack.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital
On Sun, 4 Mar 2012, Cezary Kaliszyk wrote:
Makarius once suggested an antiquotation, that does something like
'print_theorems'. I have not investigated how to implement one?
Pretty printing into latex source is not a big deal, if you are satisfied
with regular multiline output in the display
On 07/12/2011 11:15 PM, Florian Haftmann wrote:
Hi Cezary (et al),
first, thanks a lot for your efforts, this is a valuable contribution!
There are a number of obvious things that could
be done with it, like you mention Isabelle settings but also proper
use of
local theories (this would avoid
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
