Code Organisation

trunk/

cylobi -- Cyclic Logic of Bunched Implications
HiGraph -- HiGraph system
isaplib -- Generic IsaPlanner libraries
IsaPlanner -- IsaPlanner, the proof planner for Isabell. Versions of IsaPlanner for different version of Isabelle live here. e.g. IsaPlanner/IsaPlanner-2009-1 is the version of IsaPlanner for running with the late 2009 version of Isabelle called Isabelle-2009-1.
quantomatic -- Quantomatic, for reasoning about quantum computation

src/ -- source code for IsaPlanner
IsaMakefile -- An Isabelle make file to make IsaPlanner (type "isabelle make" in this directory to build IsaPlanner)
quicktest.thy -- a file to copy/paste from for playing with IsaPlanner.

benchmarks/ -- the benchmarking tools for IsaPlanner
cinfos/ -- currently holds various kinds of contextual information.
critics/ -- work on critics
dbg.ML -- a file shared by developers to debug bits in IsaPlanner, or arrive at a state to show a bug
dbg/ -- holds various debugging code, rather like a temp directory for shared code to be debugged.
examples/ -- includes example and demo files
generic/ -- IsaPlanner's generic libraries (beyond those of Isabelle), names, sets, binary relations etc.
pplan/ -- this is the underlying notion of proof, used by IsaPlanner proof plans.
interface/ -- the debugging interface for tracing IsaPlanner
libs/ -- libraries of tools, such as embeddings, terms, graphs, names.
ROOT.ML -- the file to load IsaPlanner, it just loads the appropriate theory, and that does all the work.
rstate/ -- the central part of IsaPlanner, this defines the notion of reasoning state, reasning technique, etc.
rtechn/ -- specific technique modules go in here, such as rippling, induction, etc. Each technique which needs many files has it's own directory.
sys -- low level tools for Isabelle
theories/ -- this holds the theory files, which setup the Isar theory level hooks and load IsaPlanner.