src/HOL/Modelcheck/CTL.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 17272 c63e5220ed77
child 24327 a207114007c6
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     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 theory CTL
     8 imports MuCalculus
     9 begin
    10 
    11 types
    12   'a trans  = "('a * 'a) set"
    13 
    14 constdefs
    15   CEX ::"['a trans,'a pred, 'a]=>bool"
    16   "CEX N f u == (? v. (f v & (u,v):N))"
    17   EG ::"['a trans,'a pred]=> 'a pred"
    18   "EG N f == nu (% Q. % u.(f u & CEX N Q u))"
    19 
    20 ML {* use_legacy_bindings (the_context ()) *}
    21 
    22 end