isabelle: src/HOLCF/ex/Dnat.thy@93da54c8a687 (annotated)

2570 24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	1	(* Title: HOLCF/Dnat.thy
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	2	ID: $Id$
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	3	Author: Franz Regensburger
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	4	Copyright 1993 Technische Universitaet Muenchen
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	5
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	6	Theory for the domain of natural numbers dnat = one ++ dnat
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	7	*)
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	8
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	9	Dnat = HOLCF +
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	10
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	11	domain dnat = dzero \| dsucc (dpred :: dnat)
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	12
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	13	constdefs
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	14
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	15	iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a"
10835 f4745d77e620 ` -> $ nipkow parents: 2570 diff changeset	16	"iterator == fix$(LAM h n f x . case n of dzero => x
f4745d77e620 ` -> $ nipkow parents: 2570 diff changeset	17	\| dsucc$m => f$(h$m$f$x))"
2570 24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	18
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	19	end

author	wenzelm
	Wed, 26 Sep 2001 22:24:55 +0200
changeset 11572	93da54c8a687
parent 10835	f4745d77e620
child 12035	f2ee4b5d02f2
permissions	-rw-r--r--