| author | wenzelm |
| Fri, 08 Mar 2002 16:24:06 +0100 | |
| changeset 13049 | ce180e5b7fa0 |
| parent 11703 | 6e5de8d4290a |
| permissions | -rw-r--r-- |
(* File: TLA/ex/inc/Pcount.thy Author: Stephan Merz Copyright: 1997 University of Munich Theory Name: Pcount Logic Image: TLA Data type "program counter" for the increment example. Isabelle/HOL's datatype package generates useful simplifications and case distinction tactics. *) Pcount = Main + datatype pcount = a | b | g end