src/ZF/ROOT

     http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz
   *}
   options [document = false]
   theories Confluence
 
-session "ZF-UNITY" (timing ZF) in UNITY = ZF +
+session "ZF-UNITY" (timing ZF) in UNITY = "ZF-Induct" +
   description {*
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
     ZF/UNITY proofs.