Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. CONTRIBUTORS: new proof method "argo"
  2. NEWS: new proof method "argo"
  3. use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
  4. invoke argo as part of the tried automatic proof methods
  5. new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
  6. HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
  7. HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
  8. HOL-Analysis: move gauges and (tagged) divisions to its own theory file
  9. HOL-Analysis: add cover lemma ported by L. C. Paulson
  10. more new material
  11. Generalised the type of map_poly
Changeset 63964:9f0308e80366 by boehmes:
CONTRIBUTORS: new proof method "argo"
The file was modified CONTRIBUTORS (diff)
Changeset 63963:ed98a055b9a5 by boehmes:
NEWS: new proof method "argo"
The file was modified NEWS (diff)
Changeset 63962:83a625d06e91 by boehmes:
use argo as additional SAT solver with models but no proofs, since the proof trace formats are not easily translatable
The file was addedsrc/HOL/Tools/Argo/argo_sat_solver.ML
The file was modified src/HOL/Presburger.thy (diff)
The file was modified src/HOL/SAT.thy (diff)
Changeset 63961:2fd9656c4c82 by boehmes:
invoke argo as part of the tried automatic proof methods
The file was modified src/HOL/Presburger.thy (diff)
The file was modified src/HOL/Real.thy (diff)
The file was modified src/HOL/Tools/try0.ML (diff)
Changeset 63960:3daf02070be5 by boehmes:
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
The file was addedsrc/HOL/Argo.thy
The file was addedsrc/HOL/Tools/Argo/argo_real.ML
The file was addedsrc/HOL/Tools/Argo/argo_tactic.ML
The file was addedsrc/HOL/ex/Argo_Examples.thy
The file was addedsrc/Tools/Argo/argo_cc.ML
The file was addedsrc/Tools/Argo/argo_cdcl.ML
The file was addedsrc/Tools/Argo/argo_clausify.ML
The file was addedsrc/Tools/Argo/argo_cls.ML
The file was addedsrc/Tools/Argo/argo_common.ML
The file was addedsrc/Tools/Argo/argo_core.ML
The file was addedsrc/Tools/Argo/argo_expr.ML
The file was addedsrc/Tools/Argo/argo_heap.ML
The file was addedsrc/Tools/Argo/argo_lit.ML
The file was addedsrc/Tools/Argo/argo_proof.ML
The file was addedsrc/Tools/Argo/argo_rewr.ML
The file was addedsrc/Tools/Argo/argo_simplex.ML
The file was addedsrc/Tools/Argo/argo_solver.ML
The file was addedsrc/Tools/Argo/argo_term.ML
The file was addedsrc/Tools/Argo/argo_thy.ML
The file was modified src/HOL/ROOT (diff)
The file was modified src/HOL/Real.thy (diff)
Changeset 63959:f77dca1abf1b by hoelzl:
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
The file was modified src/HOL/Analysis/Complete_Measure.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Lebesgue_Measure.thy (diff)
The file was modified src/HOL/Analysis/Measure_Space.thy (diff)
The file was modified src/HOL/Set.thy (diff)
Changeset 63958:02de4a58e210 by hoelzl:
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
The file was modified src/HOL/Analysis/Complete_Measure.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Lebesgue_Measure.thy (diff)
The file was modified src/HOL/Analysis/Measure_Space.thy (diff)
The file was modified src/HOL/Analysis/Set_Integral.thy (diff)
The file was modified src/HOL/Library/Indicator_Function.thy (diff)
Changeset 63957:c3da799b1b45 by hoelzl:
HOL-Analysis: move gauges and (tagged) divisions to its own theory file
The file was addedsrc/HOL/Analysis/Tagged_Division.thy
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
Changeset 63956:b235e845c8e8 by hoelzl:
HOL-Analysis: add cover lemma ported by L. C. Paulson
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
Changeset 63955:51a3d38d2281 by paulson _lp15@cam.ac.uk_:
more new material
The file was modified src/HOL/Analysis/Cauchy_Integral_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Derivative.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
Changeset 63954:fb03766658f4 by paulson _lp15@cam.ac.uk_:
Generalised the type of map_poly
The file was modified src/HOL/Library/Polynomial_Factorial.thy (diff)