author | wenzelm |
Thu, 19 Aug 1999 19:55:13 +0200 | |
changeset 7295 | fe09a0c5cebe |
parent 3882 | 6d7df9b98537 |
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