# HG changeset patch
# User paulson
# Date 963575820 -7200
# Node ID f0c2b71db81bf57b50a2de77dceba97864f46b1b
# Parent  5cacc383157a795c8a9403e120e9734a1df77ff6
parent should be Main

diff -r 5cacc383157a -r f0c2b71db81b src/ZF/Resid/Redex.thy
--- a/src/ZF/Resid/Redex.thy	Fri Jul 14 13:39:03 2000 +0200
+++ b/src/ZF/Resid/Redex.thy	Fri Jul 14 13:57:00 2000 +0200
@@ -5,7 +5,7 @@
     Logic Image: ZF
 *)
 
-Redex = Datatype +
+Redex = Main +
 consts
   redexes     :: i