src/HOL/Modelcheck/CTL.thy
author haftmann
Wed, 20 May 2009 10:37:37 +0200
changeset 31207 7eb05fc49b45
parent 24327 a207114007c6
child 35416 d8d7d1b785af
permissions -rw-r--r--
added generator for type copies (records)

(*  Title:      HOL/Modelcheck/CTL.thy
    ID:         $Id$
    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
    Copyright   1997  TU Muenchen
*)

theory CTL
imports MuCalculus
begin

types
  'a trans  = "('a * 'a) set"

constdefs
  CEX ::"['a trans,'a pred, 'a]=>bool"
  "CEX N f u == (? v. (f v & (u,v):N))"
  EG ::"['a trans,'a pred]=> 'a pred"
  "EG N f == nu (% Q. % u.(f u & CEX N Q u))"

end