src/HOL/Modelcheck/CTL.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 7295 fe09a0c5cebe
child 17272 c63e5220ed77
permissions -rw-r--r--
Constant "If" is now local
     1 (*  Title:      HOL/Modelcheck/CTL.thy
     2     ID:         $Id$
     3     Author:     Olaf Mueller, Jan Philipps, Robert Sandner
     4     Copyright   1997  TU Muenchen
     5 *)
     6 
     7 CTL = MuCalculus + 
     8 
     9 
    10 types
    11   'a trans  = "('a * 'a) set"
    12 
    13 consts
    14   CEX   ::"['a trans,'a pred, 'a]=>bool"
    15   EG    ::"['a trans,'a pred]=> 'a pred"
    16 
    17 defs
    18   CEX_def  "CEX N f u == (? v. (f v & (u,v):N))"
    19   EG_def   "EG N f == nu (% Q. % u.(f u & CEX N Q u))"
    20 
    21 end