src/ZF/ex/Data.thy
author lcp
Tue Mar 07 13:37:48 1995 +0100 (1995-03-07)
changeset 935 a94ef3eed456
parent 515 abcc438e7c27
child 1401 0c439768f45c
permissions -rw-r--r--
Changed Univ to Datatype in parents
lcp@515
     1
(*  Title: 	ZF/ex/Data.thy
lcp@515
     2
    ID:         $Id$
lcp@515
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@515
     4
    Copyright   1994  University of Cambridge
lcp@515
     5
lcp@515
     6
Sample datatype definition.  
lcp@515
     7
It has four contructors, of arities 0-3, and two parameters A and B.
lcp@515
     8
*)
lcp@515
     9
lcp@935
    10
Data = Datatype +
lcp@515
    11
lcp@515
    12
consts
lcp@515
    13
  data :: "[i,i] => i"
lcp@515
    14
lcp@515
    15
datatype
lcp@515
    16
  "data(A,B)" = Con0
lcp@515
    17
              | Con1 ("a: A")
lcp@515
    18
              | Con2 ("a: A", "b: B")
lcp@515
    19
              | Con3 ("a: A", "b: B", "d: data(A,B)")
lcp@515
    20
lcp@515
    21
end