--- a/src/ZF/ex/Data.thy Wed Nov 14 23:22:15 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-(* Title: ZF/ex/Data.thy
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Sample datatype definition.
-It has four contructors, of arities 0-3, and two parameters A and B.
-*)
-
-Data = Main +
-
-consts
- data :: [i,i] => i
-
-datatype
- "data(A,B)" = Con0
- | Con1 ("a \\<in> A")
- | Con2 ("a \\<in> A", "b \\<in> B")
- | Con3 ("a \\<in> A", "b \\<in> B", "d \\<in> data(A,B)")
-
-end