--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Acc.thy Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,23 @@
+(* 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