Skip to content
[Jenkins]Jenkins
log in
Success

Changes

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

Summary

  1. merged
  2. moved Interval and Interval_Approximation to isabelle
Changeset 10688:2a06a089800f by immler:
merged
Changeset 10687:c5944c920143 by immler:
moved Interval and Interval_Approximation to isabelle
The file was modified thys/Affine_Arithmetic/Affine_Approximation.thy
The file was modified thys/Affine_Arithmetic/Print.thy
The file was modified thys/Differential_Dynamic_Logic/Differential_Axioms.thy
The file was modified thys/Ordinary_Differential_Equations/Ex/Lorenz/Lorenz_Approximation.thy
The file was modified thys/Ordinary_Differential_Equations/Ex/Lorenz/Result_Elements.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/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/Example_Utilities.thy
The file was modified thys/Ordinary_Differential_Equations/Numerics/Refine_Rigorous_Numerics_Aform.thy
The file was modified thys/Taylor_Models/Experiments.thy
The file was modified thys/Taylor_Models/Horner_Eval.thy
The file was modified thys/Taylor_Models/Polynomial_Expression_Additional.thy
The file was modified thys/Taylor_Models/Taylor_Models.thy
The file was removedthys/Taylor_Models/Interval.thy
The file was removedthys/Taylor_Models/Interval_Approximation.thy

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

Summary

  1. merged
  2. add lemmas
  3. refactor Approximation.thy to use more abstract type of intervals
  4. moved theory Interval_Approximation from the AFP
  5. moved theory Interval from the AFP
  6. replace approximation oracle by less ad-hoc @{computation}s
Changeset 71039:ddd4aefc540f by immler:
merged
Changeset 71038:bd3d4702b4f2 by immler:
add lemmas
The file was modified src/HOL/Library/Interval.thy
The file was modified src/HOL/Library/Interval_Float.thy
Changeset 71037:f630f2e707a6 by immler:
refactor Approximation.thy to use more abstract type of intervals
The file was modified src/HOL/Decision_Procs/Approximation.thy
The file was modified src/HOL/Decision_Procs/Approximation_Bounds.thy
The file was modified src/HOL/Decision_Procs/approximation.ML
The file was modified src/HOL/Decision_Procs/approximation_generator.ML
The file was modified src/HOL/Library/Interval.thy
The file was modified src/HOL/Library/Interval_Float.thy
Changeset 71036:dfcc1882d05a by immler:
moved theory Interval_Approximation from the AFP
The file was addedsrc/HOL/Library/Interval_Float.thy
The file was modified src/HOL/Decision_Procs/Approximation_Bounds.thy
The file was modified src/HOL/Library/Float.thy
The file was modified src/HOL/Library/Library.thy
Changeset 71035:6fe5a0e1fa8e by immler:
moved theory Interval from the AFP
The file was addedsrc/HOL/Library/Interval.thy
The file was modified src/HOL/Library/Library.thy
Changeset 71034:e0755162093f by immler:
replace approximation oracle by less ad-hoc @{computation}s
The file was modified src/HOL/Decision_Procs/Approximation.thy
The file was modified src/HOL/Decision_Procs/approximation.ML
The file was modified src/HOL/Decision_Procs/approximation_generator.ML