author | paulson |
Thu, 11 Nov 1999 10:25:17 +0100 | |
changeset 8005 | b64d86018785 |
parent 7537 | 875754b599df |
child 8251 | 9be357df93d4 |
permissions | -rw-r--r-- |
(* 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 decr :: "(nat*nat) set" "decr == UN n. {(Suc n, n)}" Timer :: nat program "Timer == mk_program (UNIV, {decr})" end