changeset 7513 | 879ae27f5e6f |
child 7537 | 875754b599df |
7512:930e5947562d | 7513:879ae27f5e6f |
---|---|
1 (* Title: HOL/UNITY/TimerArray.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 A trivial example of reasoning about an array of processes |
|
7 *) |
|
8 |
|
9 TimerArray = PPROD + |
|
10 |
|
11 constdefs |
|
12 Timer :: nat program |
|
13 "Timer == mk_program (UNIV, {range(%n. (Suc n, n))})" |
|
14 |
|
15 end |