isabelle: src/HOLCF/ex/Dnat.thy@1379275df5cd (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"
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	16	"iterator == fix`(LAM h n f x . case n of dzero => x
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	17	\| dsucc`m => f`(h`m`f`x))"
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	18
24d7e8fb8261 added Classlib.* and Witness., oheimb* parents: diff changeset	19	end

author	wenzelm
	Mon, 16 Aug 1999 17:38:52 +0200
changeset 7215	1379275df5cd
parent 2570	24d7e8fb8261
child 10835	f4745d77e620
permissions	-rw-r--r--