src/HOL/Modelcheck/CTL.thy

Now Datatype.occs_in_prems prints the necessary warning ITSELF.

It is also easier to invoke and even works if the induction variable
is a parameter (rather than a free variable).

(*  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