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