cleanup for Fun.thy:
merged Update.{thy|ML} into Fun.{thy|ML}
moved o_def from HOL.thy to Fun.thy
added Id_def to Fun.thy
moved image_compose from Set.ML to Fun.ML
moved o_apply and o_assoc from simpdata.ML to Fun.ML
moved fun_upd_same and fun_upd_other (from Map.ML) to Fun.ML
added fun_upd_twist to Fun.ML
(* Title: HOL/Modelcheck/Example.thy
ID: $Id$
Author: Olaf Mueller, Jan Philipps, Robert Sandner
Copyright 1997 TU Muenchen
*)
Example = CTL + MCSyn +
types
state = "bool * bool * bool"
consts
INIT :: "state pred"
N :: "[state,state] => bool"
reach:: "state pred"
defs
INIT_def "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))"
N_def "N == % (x1,x2,x3) (y1,y2,y3).
(~x1 & ~x2 & ~x3 & y1 & ~y2 & ~y3) |
( x1 & ~x2 & ~x3 & ~y1 & ~y2 & ~y3) |
( x1 & ~x2 & ~x3 & y1 & y2 & y3) "
reach_def "reach == mu (%Q x. INIT x | (? y. Q y & N y x))"
end