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