changeset 13550 | 5a176b8dda84 |
parent 11868 | 56db9f3a6b3e |
child 13601 | fd3e3d6b37b2 |
--- a/src/HOL/UNITY/SubstAx.ML Thu Aug 29 16:15:11 2002 +0200 +++ b/src/HOL/UNITY/SubstAx.ML Fri Aug 30 16:42:45 2002 +0200 @@ -6,9 +6,6 @@ LeadsTo relation, restricted to the set of reachable states. *) -overload_1st_set "SubstAx.op LeadsTo"; - - (*Resembles the previous definition of LeadsTo*) Goalw [LeadsTo_def] "A LeadsTo B = {F. F : (reachable F Int A) leadsTo (reachable F Int B)}";