src/ZF/ex/Acc.thy
author lcp
Mon Dec 19 15:22:42 1994 +0100 (1994-12-19)
changeset 809 1daa0269eb5d
parent 578 efc648d29dd0
child 1401 0c439768f45c
permissions -rw-r--r--
removed quotes around "Inductive"
     1 (*  Title: 	ZF/ex/Acc.thy
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Inductive definition of acc(r)
     7 
     8 See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
     9 Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
    10 *)
    11 
    12 Acc = WF + Inductive +
    13 
    14 consts
    15   acc :: "i=>i"
    16 
    17 inductive
    18   domains "acc(r)" <= "field(r)"
    19   intrs
    20     vimage  "[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"
    21   monos     "[Pow_mono]"
    22 
    23 end