src/ZF/ex/Data.thy
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 515 abcc438e7c27
child 935 a94ef3eed456
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
     1 (*  Title: 	ZF/ex/Data.thy
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Sample datatype definition.  
     7 It has four contructors, of arities 0-3, and two parameters A and B.
     8 *)
     9 
    10 Data = Univ +
    11 
    12 consts
    13   data :: "[i,i] => i"
    14 
    15 datatype
    16   "data(A,B)" = Con0
    17               | Con1 ("a: A")
    18               | Con2 ("a: A", "b: B")
    19               | Con3 ("a: A", "b: B", "d: data(A,B)")
    20 
    21 end