isabelle: src/HOLCF/ex/Dnat.thy@4f2e6c87a57f (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	paulson
	Tue, 24 Apr 2001 12:19:58 +0200
changeset 11265	4f2e6c87a57f
parent 10835	f4745d77e620
child 12035	f2ee4b5d02f2
permissions	-rw-r--r--