diff -r ab2c867829ec -r abcc438e7c27 src/ZF/ex/Data.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Data.thy	Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,21 @@
+(*  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 = Univ +
+
+consts
+  data :: "[i,i] => i"
+
+datatype
+  "data(A,B)" = Con0
+              | Con1 ("a: A")
+              | Con2 ("a: A", "b: B")
+              | Con3 ("a: A", "b: B", "d: data(A,B)")
+
+end