Skip to content
Failed

Changes

Summary

  1. adapted to L2_set
Changeset 8584:2238268f1eb8 by nipkow:
adapted to L2_set
The file was modified thys/Affine_Arithmetic/Executable_Euclidean_Space.thy (diff)
The file was modified thys/Affine_Arithmetic/Floatarith_Expression.thy (diff)
The file was modified thys/Differential_Dynamic_Logic/Lib.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Ex/Lorenz/Lorenz_Approximation.thy (diff)
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)
The file was modified thys/Ordinary_Differential_Equations/Numerics/Refine_Vector_List.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Numerics/Transfer_Euclidean_Space_Vector.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/ODE_Auxiliarities.thy (diff)
The file was modified thys/Perron_Frobenius/Perron_Frobenius_Aux.thy (diff)
The file was modified thys/Perron_Frobenius/Perron_Frobenius_Irreducible.thy (diff)
The file was modified thys/Tarskis_Geometry/Hyperbolic_Tarski.thy (diff)