[Pkg-ocaml-maint-commits] [hol-light] 02/06: Merge tag 'upstream/20170917'
Hendrik Tews
hendrik-guest at moszumanska.debian.org
Sun Oct 29 21:00:10 UTC 2017
This is an automated email from the git hooks/post-receive script.
hendrik-guest pushed a commit to branch master
in repository hol-light.
commit 7b77dc8b211e8f06e95b733db077bbf3e7913f6d
Merge: e4242ac 64d942d
Author: Hendrik Tews <hendrik at askra.de>
Date: Sun Sep 24 22:46:53 2017 +0200
Merge tag 'upstream/20170917'
Upstream version 20170917
100/circle.ml | 6 +-
100/inclusion_exclusion.ml | 2 +-
100/lagrange.ml | 1 +
100/liouville.ml | 26 -
100/minkowski.ml | 102 +-
100/pnt.ml | 24 +-
100/sqrt.ml | 1 -
Boyer_Moore/README | 2 +-
Boyer_Moore/counterexample.ml | 2 +-
Boyer_Moore/definitions.ml | 2 +-
Boyer_Moore/environment.ml | 4 +-
Boyer_Moore/equalities.ml | 11 +-
Boyer_Moore/generalize.ml | 55 +-
Boyer_Moore/induction.ml | 4 +-
Boyer_Moore/irrelevance.ml | 7 +-
Boyer_Moore/main.ml | 152 +-
Boyer_Moore/make.ml | 8 +-
Boyer_Moore/shells.ml | 14 +-
Boyer_Moore/terms_and_clauses.ml | 22 +-
Boyer_Moore/waterfall.ml | 140 +-
CHANGES | 1191 +-
Complex/complex_grobner.ml | 6 +-
Complex/complexnumbers.ml | 4 +-
Complex/quelim.ml | 4 +-
Examples/borsuk.ml | 2 +-
Examples/division_algebras.ml | 196 +-
Examples/kb.ml | 2 +-
Examples/machin.ml | 2 +-
Examples/pell.ml | 2 +-
Examples/prover9.ml | 4 +-
Examples/sos.ml | 2 +-
Formal_ineqs/README.md | 12 +
Formal_ineqs/README.txt | 8 -
Formal_ineqs/arith/arith_cache.hl | 74 +-
Formal_ineqs/arith/{float.hl => arith_float.hl} | 8075 ++++++-----
Formal_ineqs/arith/arith_nat.hl | 106 +
Formal_ineqs/arith/arith_num.hl | 552 +-
Formal_ineqs/arith/eval_interval.hl | 201 +-
Formal_ineqs/arith/float_atn.hl | 582 -
Formal_ineqs/arith/float_pow.hl | 526 +
Formal_ineqs/arith/float_theory.hl | 206 +-
Formal_ineqs/arith/interval_arith.hl | 127 +-
Formal_ineqs/arith/more_float.hl | 1087 +-
Formal_ineqs/arith/nat.hl | 102 -
Formal_ineqs/arith/num_exp_theory.hl | 502 +-
Formal_ineqs/arith_options.hl | 53 +-
Formal_ineqs/docs/FormalVerifier.pdf | Bin 223139 -> 203253 bytes
Formal_ineqs/docs/FormalVerifier.tex | 47 +-
Formal_ineqs/examples.hl | 19 +-
Formal_ineqs/examples_flyspeck.hl | 122 +-
Formal_ineqs/examples_other.hl | 35 +
Formal_ineqs/examples_poly.hl | 16 +-
Formal_ineqs/informal/informal_arith.hl | 805 --
Formal_ineqs/informal/informal_asn_acs.hl | 169 +
Formal_ineqs/informal/informal_atn.hl | 228 +
Formal_ineqs/informal/informal_eval_interval.hl | 208 +-
Formal_ineqs/informal/informal_exp.hl | 241 +
Formal_ineqs/informal/informal_float.hl | 526 +
Formal_ineqs/informal/informal_interval.hl | 248 +
Formal_ineqs/informal/informal_log.hl | 123 +
Formal_ineqs/informal/informal_m_taylor.hl | 403 -
Formal_ineqs/informal/informal_m_verifier.hl | 302 -
Formal_ineqs/informal/informal_matan.hl | 206 +
Formal_ineqs/informal/informal_nat.hl | 167 +
Formal_ineqs/informal/informal_poly.hl | 102 +
Formal_ineqs/informal/informal_search.hl | 298 +
Formal_ineqs/informal/informal_sin_cos.hl | 412 +
Formal_ineqs/informal/informal_taylor.hl | 667 +
Formal_ineqs/informal/informal_verifier.hl | 332 +
.../jordan/parse_ext_override_interface.hl | 213 -
Formal_ineqs/jordan/real_ext.hl | 303 -
Formal_ineqs/jordan/refinement.hl | 79 -
Formal_ineqs/jordan/taylor_atn.hl | 917 --
Formal_ineqs/lib/ipow.hl | 447 +
Formal_ineqs/lib/ssrbool-compiled.hl | 759 -
Formal_ineqs/lib/ssrbool.hl | 767 +
Formal_ineqs/lib/ssreflect/sections.hl | 264 +-
Formal_ineqs/lib/ssreflect/ssreflect.hl | 611 +-
Formal_ineqs/lib/ssrfun-compiled.hl | 304 -
Formal_ineqs/lib/ssrfun.hl | 375 +
Formal_ineqs/lib/ssrnat-compiled.hl | 1634 ---
Formal_ineqs/lib/ssrnat.hl | 2222 +++
Formal_ineqs/list/list_conversions.hl | 180 +-
Formal_ineqs/list/list_float.hl | 404 +-
Formal_ineqs/list/more_list.hl | 262 +-
Formal_ineqs/make.ml | 48 -
Formal_ineqs/misc/{misc.hl => misc_functions.hl} | 143 +-
Formal_ineqs/misc/{vars.hl => misc_vars.hl} | 300 +-
.../interval_m/report.ml => misc/report.hl} | 26 +-
Formal_ineqs/taylor/m_taylor.hl | 2978 ++--
Formal_ineqs/taylor/m_taylor_arith.hl | 2837 +++-
Formal_ineqs/taylor/m_taylor_arith2.hl | 897 +-
.../taylor/theory/multivariate_taylor-compiled.hl | 3967 ++---
Formal_ineqs/taylor/theory/multivariate_taylor.vhl | 1119 +-
.../taylor/theory/taylor_interval-compiled.hl | 4113 ++++--
Formal_ineqs/taylor/theory/taylor_interval.vhl | 1542 +-
Formal_ineqs/tests/data/gen_nat_data.py | 27 +
Formal_ineqs/tests/float_data.hl | 40 +
Formal_ineqs/tests/log.hl | 76 +
Formal_ineqs/tests/nat_test.hl | 200 +
Formal_ineqs/tests/results.hl | 109 +
Formal_ineqs/tests/test_utils.hl | 185 +
Formal_ineqs/trig/asn_acs_eval.hl | 413 +
Formal_ineqs/trig/atn.hl | 309 +
Formal_ineqs/trig/atn_eval.hl | 472 +
Formal_ineqs/trig/cos_bounds_eval.hl | 196 +
Formal_ineqs/trig/cos_eval.hl | 1238 ++
Formal_ineqs/trig/exp_eval.hl | 414 +
Formal_ineqs/trig/exp_log.hl | 313 +
Formal_ineqs/trig/log_eval.hl | 205 +
Formal_ineqs/trig/matan.hl | 712 +
Formal_ineqs/trig/matan_eval.hl | 379 +
Formal_ineqs/trig/poly.hl | 231 +
Formal_ineqs/trig/poly_eval.hl | 372 +
Formal_ineqs/trig/series.hl | 1298 ++
Formal_ineqs/trig/sin_cos.hl | 298 +
Formal_ineqs/trig/sin_eval.hl | 87 +
Formal_ineqs/trig/test.hl | 89 +
Formal_ineqs/trig/unused.hl | 240 +
Formal_ineqs/verifier/certificate.hl | 284 +
Formal_ineqs/verifier/interval_m/interval.ml | 173 -
Formal_ineqs/verifier/interval_m/line_interval.ml | 114 -
Formal_ineqs/verifier/interval_m/recurse.ml | 315 -
Formal_ineqs/verifier/interval_m/recurse0.ml | 152 -
Formal_ineqs/verifier/interval_m/taylor.ml | 376 -
Formal_ineqs/verifier/interval_m/types.ml | 52 -
Formal_ineqs/verifier/interval_m/univariate.ml | 107 -
Formal_ineqs/verifier/interval_m/verifier.ml | 305 -
Formal_ineqs/verifier/m_verifier.hl | 1466 +-
Formal_ineqs/verifier/m_verifier_build.hl | 193 +-
Formal_ineqs/verifier/m_verifier_main.hl | 731 +-
Formal_ineqs/verifier_options.hl | 36 +-
Functionspaces/cfunspace.ml | 89 +-
IEEE/fixed_thms.hl | 2 +-
IsabelleLight/README | 70 +-
IsabelleLight/meta_rules.ml | 174 +-
IsabelleLight/new_tactics.ml | 255 +-
IsabelleLight/support.ml | 149 +-
Jordan/jordan_curve_theorem.ml | 61 +-
Jordan/metric_spaces.ml | 17 +-
Jordan/num_ext_nabs.ml | 2 +-
Jordan/real_ext.ml | 2 +-
Jordan/tactics_ext2.ml | 10 +-
Library/analysis.ml | 88 +-
Library/card.ml | 601 +-
Library/floor.ml | 105 +-
Library/frag.ml | 418 +
Library/grouptheory.ml | 3037 ++++
Library/pocklington.ml | 10 +-
Library/pratt.ml | 4 +-
Library/prime.ml | 31 +
Library/transc.ml | 233 +-
Makefile | 19 +-
Minisat/minisat_parse.ml | 10 +-
Multivariate/canal.ml | 30 +-
Multivariate/cauchy.ml | 28 +-
Multivariate/complex_database.ml | 1280 +-
Multivariate/complexes.ml | 16 +-
Multivariate/convex.ml | 51 +-
Multivariate/cvectors.ml | 11 +-
Multivariate/degree.ml | 314 +-
Multivariate/derivatives.ml | 26 +-
Multivariate/determinants.ml | 186 +-
Multivariate/flyspeck.ml | 85 +-
Multivariate/geom.ml | 24 +-
Multivariate/integration.ml | 148 +-
Multivariate/lpspaces.ml | 107 +-
Multivariate/measure.ml | 252 +-
Multivariate/metric.ml | 14340 ++++++++++++++++++-
Multivariate/misc.ml | 949 +-
Multivariate/moretop.ml | 214 +-
Multivariate/multivariate_database.ml | 1264 +-
Multivariate/paths.ml | 983 +-
Multivariate/polytope.ml | 32 +-
Multivariate/realanalysis.ml | 2358 ++-
Multivariate/topology.ml | 5889 +++++---
Multivariate/transcendentals.ml | 134 +-
Multivariate/vectors.ml | 564 +-
Quaternions/qanal.hl | 4 +-
Quaternions/qnormalizer.hl | 21 +-
Rqe/asym.ml | 4 +-
Rqe/inferisign_thms.ml | 2 +-
Rqe/inferpsign_thms.ml | 2 +-
Tutorial/Custom_inference_rules.ml | 2 +-
Tutorial/all.ml | 2 +-
arith.ml | 28 +
calc_int.ml | 2 +-
calc_rat.ml | 62 +-
cart.ml | 33 +-
class.ml | 2 +-
database.ml | 188 +-
drule.ml | 4 +-
grobner.ml | 10 +-
holtest | 2 +
holtest.mk | 99 +-
ind_types.ml | 4 +-
int.ml | 20 +-
lists.ml | 39 +-
nums.ml | 8 +-
pa_j_4.xx_7.xx.ml | 2971 ++++
pair.ml | 27 +-
parser.ml | 8 +-
printer.ml | 41 +-
real.ml | 477 +-
sets.ml | 881 +-
tactics.ml | 2 +-
206 files changed, 71917 insertions(+), 27507 deletions(-)
--
Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/hol-light.git
More information about the Pkg-ocaml-maint-commits
mailing list