src/ZF/ex/Data.thy
author paulson
Mon May 21 14:36:24 2001 +0200 (2001-05-21)
changeset 11316 b4e71bd751e4
parent 1478 2b8c2a7547ab
child 11354 9b80fe19407f
permissions -rw-r--r--
X-symbols for set theory
clasohm@1478
     1
(*  Title:      ZF/ex/Data.thy
lcp@515
     2
    ID:         $Id$
clasohm@1478
     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
clasohm@1401
    13
  data :: [i,i] => i
lcp@515
    14
lcp@515
    15
datatype
lcp@515
    16
  "data(A,B)" = Con0
paulson@11316
    17
              | Con1 ("a \\<in> A")
paulson@11316
    18
              | Con2 ("a \\<in> A", "b \\<in> B")
paulson@11316
    19
              | Con3 ("a \\<in> A", "b \\<in> B", "d \\<in> data(A,B)")
lcp@515
    20
lcp@515
    21
end