Summary
- fixed proof WRT DIM_positive being a simprule
The file was modified | thys/Ordinary_Differential_Equations/IVP/Picard_Lindeloef_Qualitative.thy (diff) |
The file was modified | thys/Ordinary_Differential_Equations/IVP/Picard_Lindeloef_Qualitative.thy (diff) |