src/HOLCF/explicit_domains/Dnat2.thy
changeset 2679 3eac428cdd1b
parent 2678 d5fe793293ac
child 2680 20fa49e610ca
     1.1 --- a/src/HOLCF/explicit_domains/Dnat2.thy	Mon Feb 24 09:46:12 1997 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,31 +0,0 @@
     1.4 -(*  Title:      HOLCF/Dnat2.thy
     1.5 -    ID:         $Id$
     1.6 -    Author:     Franz Regensburger
     1.7 -    Copyright   1993 Technische Universitaet Muenchen
     1.8 -
     1.9 -NOT SUPPORTED ANY MORE. USE HOLCF/ex/Dnat.thy INSTEAD.
    1.10 -
    1.11 -Additional constants for dnat
    1.12 -
    1.13 -*)
    1.14 -
    1.15 -Dnat2 = Dnat +
    1.16 -
    1.17 -consts
    1.18 -
    1.19 -iterator        :: "dnat -> ('a -> 'a) -> 'a -> 'a"
    1.20 -
    1.21 -
    1.22 -defs
    1.23 -
    1.24 -iterator_def    "iterator == fix`(LAM h n f x.
    1.25 -                        dnat_when `x `(LAM m.f`(h`m`f`x)) `n)"
    1.26 -end
    1.27 -
    1.28 -(*
    1.29 -
    1.30 -                iterator`UU`f`x = UU
    1.31 -                iterator`dzero`f`x = x
    1.32 -      n~=UU --> iterator`(dsucc`n)`f`x = f`(iterator`n`f`x)
    1.33 -*)
    1.34 -