equal
deleted
inserted
replaced
|
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 |