Summary
- updated proofs because distance_attains_inf is now expressed using "obtains"
The file was modified | thys/Ordinary_Differential_Equations/IVP/Initial_Value_Problem.thy (diff) |
The file was modified | thys/Ordinary_Differential_Equations/IVP/Picard_Lindeloef_Qualitative.thy (diff) |