author | wenzelm |
Thu, 06 Dec 2001 00:39:40 +0100 | |
changeset 12397 | 6766aa05e4eb |
parent 7295 | fe09a0c5cebe |
child 17272 | c63e5220ed77 |
permissions | -rw-r--r-- |
(* Title: HOL/Modelcheck/CTL.thy ID: $Id$ Author: Olaf Mueller, Jan Philipps, Robert Sandner Copyright 1997 TU Muenchen *) CTL = MuCalculus + types 'a trans = "('a * 'a) set" consts CEX ::"['a trans,'a pred, 'a]=>bool" EG ::"['a trans,'a pred]=> 'a pred" defs CEX_def "CEX N f u == (? v. (f v & (u,v):N))" EG_def "EG N f == nu (% Q. % u.(f u & CEX N Q u))" end