README for proofs for the paper
Well-Founded Unions
by Jeremy Dawson, Nachum Dershowitz, Rajeev Gore
Monday 22 January  15:19:38 AEDT 2018

This file is ~/isabelle/2005/gen/tripartite-README

This directory contains inter alia the proofs for results in the paper.
Key files are tripartite.{ML,thy},
but also definitions and results for well-foundedness of unions of relations
are in {Wfss,WfUn}.{thy,ML}.
The proofs may also use other theories whose files are found in this
directory, namely 
Gen, Cnv, HOL_Gen, HOL_Ths, Wfss, WfUn, tripartite 

The files are to be used with Isabelle 2005 (we proved some of the relevant 
definitions and results, such as the Jumping theorem then,
and, sadly, more recent versions of Isabelle are highly incompatible).

Isabelle 2005 was written to work with Poly/ML 4.1.4, which has also been
superseded.  A version of Isabelle 2005 which works on recent versions of
Poly/ML is to be found in ~/Isabelle2005-for-PolyML-5.6,
with instructions to build and install it in
~/Isabelle2005-for-PolyML-5.6/INSTALL