Work log 2016-08-08

Some scripts not givingutput :(

Conflicts when adding multiple copies of a haskell pkg to an environment.

Raw output of TIP isn’t accepted by isabelle console, need to comment out some breaking definitions.

Running Isabelle is a bit of a pain.

From the console of build scripts:

echo 'use_thy "A";' | isabelle console

This will load/build A.thy

For IsaPlanner, add -d /path/to/contrib/IsaPlanner and -l HOL-IsaPlannerSession to use the augmented logic.

Trying the IsaCoSy examples, requires (or seems to) embedding ML code into the .thy file using ML {* ... *}