author | nipkow |
Wed, 29 Nov 2000 17:23:27 +0100 | |
changeset 10539 | 5929460a41df |
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