diff -r f66d61f5439d -r 0960686df575 Static.thy --- a/Static.thy Thu Sep 12 19:00:26 2013 +0800 +++ b/Static.thy Tue Sep 24 14:02:15 2013 +0800 @@ -482,7 +482,7 @@ | _ \ sobj = sobj')}" - +(* no del (* all reachable static states(sobjects set) *) inductive_set static :: "t_static_state set" where