isabelle: src/HOL/UNITY/TimerArray.thy@0a604b2fc2b1 (annotated)

7513 879ae27f5e6f new example HOL/UNITY/TimerArray paulson parents: diff changeset	1	(* Title: HOL/UNITY/TimerArray.thy
879ae27f5e6f new example HOL/UNITY/TimerArray paulson parents: diff changeset	2	ID: $Id$
879ae27f5e6f new example HOL/UNITY/TimerArray paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
879ae27f5e6f new example HOL/UNITY/TimerArray paulson parents: diff changeset	4	Copyright 1998 University of Cambridge
879ae27f5e6f new example HOL/UNITY/TimerArray paulson parents: diff changeset	5
879ae27f5e6f new example HOL/UNITY/TimerArray paulson parents: diff changeset	6	A trivial example of reasoning about an array of processes
879ae27f5e6f new example HOL/UNITY/TimerArray paulson parents: diff changeset	7	*)
879ae27f5e6f new example HOL/UNITY/TimerArray paulson parents: diff changeset	8
879ae27f5e6f new example HOL/UNITY/TimerArray paulson parents: diff changeset	9	TimerArray = PPROD +
879ae27f5e6f new example HOL/UNITY/TimerArray paulson parents: diff changeset	10
879ae27f5e6f new example HOL/UNITY/TimerArray paulson parents: diff changeset	11	constdefs
7537 875754b599df working snapshot paulson parents: 7513 diff changeset	12	decr :: "(nat*nat) set"
875754b599df working snapshot paulson parents: 7513 diff changeset	13	"decr == UN n. {(Suc n, n)}"
875754b599df working snapshot paulson parents: 7513 diff changeset	14
7513 879ae27f5e6f new example HOL/UNITY/TimerArray paulson parents: diff changeset	15	Timer :: nat program
7537 875754b599df working snapshot paulson parents: 7513 diff changeset	16	"Timer == mk_program (UNIV, {decr})"
7513 879ae27f5e6f new example HOL/UNITY/TimerArray paulson parents: diff changeset	17
879ae27f5e6f new example HOL/UNITY/TimerArray paulson parents: diff changeset	18	end

author	wenzelm
	Sun, 31 Oct 1999 20:11:23 +0100
changeset 7990	0a604b2fc2b1
parent 7537	875754b599df
child 8251	9be357df93d4
permissions	-rw-r--r--