src/HOL/TLA/Inc/Pcount.thy
author wenzelm
Fri Oct 05 23:58:52 2001 +0200 (2001-10-05)
changeset 11703 6e5de8d4290a
parent 5184 9b8547a9496a
permissions -rw-r--r--
tuned;
     1 (* 
     2     File:	 TLA/ex/inc/Pcount.thy
     3     Author:      Stephan Merz
     4     Copyright:   1997 University of Munich
     5 
     6     Theory Name: Pcount
     7     Logic Image: TLA
     8 
     9 Data type "program counter" for the increment example.
    10 Isabelle/HOL's datatype package generates useful simplifications
    11 and case distinction tactics.
    12 *)
    13 
    14 Pcount  =  Main +
    15 
    16 datatype pcount = a | b | g
    17 
    18 end