changeset 7513 | 879ae27f5e6f |
child 7537 | 875754b599df |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/UNITY/TimerArray.thy Wed Sep 08 15:37:31 1999 +0200 @@ -0,0 +1,15 @@ +(* Title: HOL/UNITY/TimerArray.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1998 University of Cambridge + +A trivial example of reasoning about an array of processes +*) + +TimerArray = PPROD + + +constdefs + Timer :: nat program + "Timer == mk_program (UNIV, {range(%n. (Suc n, n))})" + +end