author | wenzelm |
Mon, 03 May 1999 10:57:14 +0200 | |
changeset 6563 | 128cf997c768 |
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