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;
wenzelm@3807
     1
(* 
wenzelm@3807
     2
    File:	 TLA/ex/inc/Pcount.thy
wenzelm@3807
     3
    Author:      Stephan Merz
wenzelm@3807
     4
    Copyright:   1997 University of Munich
wenzelm@3807
     5
wenzelm@3807
     6
    Theory Name: Pcount
wenzelm@3807
     7
    Logic Image: TLA
wenzelm@3807
     8
wenzelm@3807
     9
Data type "program counter" for the increment example.
wenzelm@3807
    10
Isabelle/HOL's datatype package generates useful simplifications
wenzelm@3807
    11
and case distinction tactics.
wenzelm@3807
    12
*)
wenzelm@3807
    13
wenzelm@11703
    14
Pcount  =  Main +
wenzelm@3807
    15
wenzelm@3807
    16
datatype pcount = a | b | g
wenzelm@3807
    17
wenzelm@3807
    18
end