changeset 6295 | 351b3c2b0d83 |
parent 6012 | 1894bfc4aee9 |
child 6535 | 880f31a62784 |
--- a/src/HOL/UNITY/Reach.thy Mon Mar 01 18:37:52 1999 +0100 +++ b/src/HOL/UNITY/Reach.thy Mon Mar 01 18:38:43 1999 +0100 @@ -24,7 +24,7 @@ "asgt u v == {(s,s'). s' = s(v:= s u | s v)}" Rprg :: state program - "Rprg == mk_program (UNIV, {%v. v=init}, UN (u,v): edges. {asgt u v})" + "Rprg == mk_program ({%v. v=init}, UN (u,v): edges. {asgt u v})" reach_invariant :: state set "reach_invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}"