author | wenzelm |
Thu, 06 Dec 2001 00:39:40 +0100 | |
changeset 12397 | 6766aa05e4eb |
parent 6466 | 2eba94dc5951 |
child 17272 | c63e5220ed77 |
permissions | -rw-r--r-- |
(* Title: HOL/Modelcheck/MuckeExample2.thy ID: $Id$ Author: Olaf Mueller, Jan Philipps, Robert Sandner Copyright 1997 TU Muenchen *) MuckeExample2 = MuckeSyn + consts Init :: "bool pred" R :: "[bool,bool] => bool" Reach :: "bool pred" Reach2:: "bool pred" defs Init_def " Init x == x" R_def "R x y == (x & ~y) | (~x & y)" Reach_def "Reach == mu (%Q x. Init x | (? y. Q y & R y x))" Reach2_def "Reach2 == mu (%Q x. Reach x | (? y. Q y & R y x))" end