Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Changes from Mercurial (hg https://bitbucket.org/isa-afp/afp-devel/ default)

Summary

  1. moved options and initalization to implementation, easier to work with different ODEs: everything in the implementation is explicitly parameterized by ode_ops
Changeset 10221:ddbc38c5dfbf by immler:
moved options and initalization to implementation, easier to work with different ODEs: everything in the implementation is explicitly parameterized by ode_ops
The file was addedthys/Ordinary_Differential_Equations/IVP/Flow_Congs.thy
The file was addedthys/Ordinary_Differential_Equations/Refinement/Refine_ScaleR2.thy
The file was modified thys/Ordinary_Differential_Equations/Ex/Examples_ARCH_COMP.thy
The file was modified thys/Ordinary_Differential_Equations/Ex/Examples_Integral.thy
The file was modified thys/Ordinary_Differential_Equations/Ex/Examples_One_Step_Method.thy
The file was modified thys/Ordinary_Differential_Equations/Ex/Examples_Poincare_Map.thy
The file was modified thys/Ordinary_Differential_Equations/Ex/Lorenz/Lorenz_Approximation.thy
The file was modified thys/Ordinary_Differential_Equations/Numerics/Abstract_Reachability_Analysis.thy
The file was modified thys/Ordinary_Differential_Equations/Numerics/Abstract_Reachability_Analysis_C1.thy
The file was modified thys/Ordinary_Differential_Equations/Numerics/Abstract_Rigorous_Numerics.thy
The file was modified thys/Ordinary_Differential_Equations/Numerics/Concrete_Reachability_Analysis.thy
The file was modified thys/Ordinary_Differential_Equations/Numerics/Concrete_Reachability_Analysis_C1.thy
The file was modified thys/Ordinary_Differential_Equations/Numerics/Concrete_Rigorous_Numerics.thy
The file was modified thys/Ordinary_Differential_Equations/Numerics/Example_Utilities.thy
The file was modified thys/Ordinary_Differential_Equations/Numerics/Init_ODE_Solver.thy
The file was modified thys/Ordinary_Differential_Equations/Numerics/Refine_Reachability_Analysis.thy
The file was modified thys/Ordinary_Differential_Equations/Numerics/Refine_Reachability_Analysis_C1.thy
The file was modified thys/Ordinary_Differential_Equations/Numerics/Refine_Rigorous_Numerics_Aform.thy
The file was modified thys/Ordinary_Differential_Equations/ODE_Analysis.thy
The file was modified thys/Ordinary_Differential_Equations/Refinement/Autoref_Misc.thy
The file was modified thys/Ordinary_Differential_Equations/Refinement/Enclosure_Operations.thy
The file was modified thys/Ordinary_Differential_Equations/Refinement/Refine_Default.thy
The file was modified thys/Ordinary_Differential_Equations/Refinement/Refine_Info.thy
The file was modified thys/Ordinary_Differential_Equations/Refinement/Refine_Intersection.thy
The file was modified thys/Ordinary_Differential_Equations/Refinement/Refine_Interval.thy
The file was modified thys/Ordinary_Differential_Equations/Refinement/Refine_Invar.thy
The file was modified thys/Ordinary_Differential_Equations/Refinement/Refine_Phantom.thy
The file was modified thys/Ordinary_Differential_Equations/Refinement/Refine_String.thy
The file was modified thys/Ordinary_Differential_Equations/Refinement/Refine_Vector_List.thy
The file was modified thys/Ordinary_Differential_Equations/Refinement/Weak_Set.thy