author | oheimb |
Mon, 27 Apr 1998 19:30:40 +0200 | |
changeset 4837 | eab729051897 |
parent 4836 | fc5773ae2790 |
child 4838 | 196100237656 |
--- a/src/HOL/UNITY/Traces.thy Mon Apr 27 19:29:19 1998 +0200 +++ b/src/HOL/UNITY/Traces.thy Mon Apr 27 19:30:40 1998 +0200 @@ -15,7 +15,6 @@ inductive "reachable Init Acts" intrs - (*Initial trace is empty*) Init "s: Init ==> s : reachable Init Acts" Acts "[| act: Acts; s : reachable Init Acts; (s,s'): act |]