## About 

isaplib is Standard ML (SML) library, built on the code-base of [Isabelle](http://www.cl.cam.ac.uk/research/hvg/Isabelle/), with some of the Isabelle-specifics removed, and some additional libraries from [IsaPlanner](http://dream.inf.ed.ac.uk/projects/isaplanner/) added. It currently uses some pretty printing code specific to [PolyML](http://www.polyml.org/), but could fairly easily be ported to other SML implementations. This library is used by [Quantomatic](http://dream.inf.ed.ac.uk/projects/quantomatic/) and [IsaPlanner](http://dream.inf.ed.ac.uk/projects/isaplanner/) related projects.

## Building outside of Isabelle

This is for when you do not have Isabelle installed. e.g. for Quantomatic. Assuming you have [PolyML](http://www.polyml.org/) installed and in the path, you can run "make" from the command line. This will create a PolyML heap image called `all.polyml-heap` in the `heaps` subdirectory. 

## Building on top of Isabelle

This is for when you have Isabelle installed (see http://www.cl.cam.ac.uk/research/hvg/isabelle/index.html) and you want to load up isaplib's additional libraries.
1. Place the isaplib directory in Isabelle's contrib directory, or just clone the isaplib repository at that location with the command:  
git clone [email protected]:iislucas/isaplib.git
2. New theories you develop can then inherrit from "~~/contrib/isaplib/isabelle/isaplib"

## LICENCE and DISCLAIMER

This software is under a combination of the Lesser GNU General Public License (GPL) and a similar license from the University of Cambridge. This software is provided "as is": you use the software at your own risk and we make no warranties of any sort. See the file called LICENCE for more information on the licence and disclaimer.