# HG changeset patch
# User lcp
# Date 775387537 -7200
# Node ID e2f00c943fa522be4010b7ac15af3c8395c4e6a2
# Parent  7bc980c7585e15dbd569ebee591b680c13747d2d
ZF/constructor.thy: now specifies intr_elim as its parent; previously had
ind_syntax, which was not sufficient.

diff -r 7bc980c7585e -r e2f00c943fa5 src/ZF/constructor.thy
--- a/src/ZF/constructor.thy	Wed Jul 27 19:08:14 1994 +0200
+++ b/src/ZF/constructor.thy	Thu Jul 28 11:25:37 1994 +0200
@@ -1,3 +1,3 @@
 (*Dummy theory to document dependencies *)
 
-constructor = "ind_syntax"
\ No newline at end of file
+constructor = "intr_elim"
\ No newline at end of file