src/ZF/ex/Acc.thy
author clasohm
Tue, 06 Feb 1996 12:27:17 +0100
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 6117 f9aad8ccd590
permissions -rw-r--r--
expanded tabs

(*  Title:      ZF/ex/Acc.thy
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1994  University of Cambridge

Inductive definition of acc(r)

See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
*)

Acc = WF + Inductive +

consts
  acc :: i=>i

inductive
  domains "acc(r)" <= "field(r)"
  intrs
    vimage  "[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"
  monos     "[Pow_mono]"

end