Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/TLA/Inc/Pcount.thy
author wenzelm
Wed, 08 Oct 1997 11:50:33 +0200
changeset 3807 82a99b090d9d
child 5184 9b8547a9496a
permissions -rw-r--r--
A formalization of TLA in HOL -- by Stephan Merz;

(* 
    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  =  HOL + Arith +

datatype pcount = a | b | g

end

ML
isabelle