GitHub - object-logics/haskabelle: Haskabelle is a converter from Haskell source files to Isabelle/HOL theories implemented in Haskell itself.

object-logics / haskabelle Public

forked from cartazio/haskabelle

Notifications You must be signed in to change notification settings
Fork 3
Star 0

Haskabelle is a converter from Haskell source files to Isabelle/HOL theories implemented in Haskell itself.

isabelle.in.tum.de/website-Isabelle2016-1/haskabelle.html

0 stars 4 forks Branches Tags Activity

Star

Notifications

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 651 Commits
Importer		Importer
admin		admin
default		default
doc-src		doc-src
doc		doc
etc		etc
ex		ex
lib		lib
.hgignore		.hgignore
COPYRIGHT		COPYRIGHT
Main.hs		Main.hs
README		README

Repository files navigation

This is Haskabelle, an importer from Haskell source files
to Isabelle/HOL Isar theories.

An overview how to use it can be found in the manual

    doc/haskabelle.pdf

If this is not present, you have to build it first;  for this you need
a source (!) distribution of Isabelle2009-2, as available from

    http://isabelle.in.tum.de/repos/isabelle/rev/!!!FIXME!!!

See further

    http://isabelle.in.tum.de/

for general hints on Isabelle2009-2.

Then, invoke

    admin/builddoc

By default, this uses the Isabelle version accessible on your PATH.
Set shell variable ISABELLE_TOOL explicitly if this does not use 
the desired Isabelle version.

Sources of Haskabelle itself are available via mercurial:

    https://isabelle.in.tum.de/repos/haskabelle