author | haftmann |
Mon, 01 Mar 2010 13:40:23 +0100 | |
changeset 35416 | d8d7d1b785af |
parent 24327 | a207114007c6 |
permissions | -rw-r--r-- |
(* Title: HOL/Modelcheck/CTL.thy Author: Olaf Mueller, Jan Philipps, Robert Sandner Copyright 1997 TU Muenchen *) theory CTL imports MuCalculus begin types 'a trans = "('a * 'a) set" definition CEX :: "['a trans,'a pred, 'a]=>bool" where "CEX N f u == (? v. (f v & (u,v):N))" definition EG ::"['a trans,'a pred]=> 'a pred" where "EG N f == nu (% Q. % u.(f u & CEX N Q u))" end