[Pkg-ocaml-maint-commits] [hol-light] branch upstream updated (991870c -> 5c800a2)
Hendrik Tews
hendrik-guest at moszumanska.debian.org
Sun Oct 29 21:00:12 UTC 2017
This is an automated email from the git hooks/post-receive script.
hendrik-guest pushed a change to branch upstream
in repository hol-light.
from 991870c Imported Upstream version 20170109
new 64d942d New upstream version 20170917
new 5c800a2 New upstream version 20171023
The 2 revisions listed above as "new" are entirely new to this
repository and will be described in separate emails. The revisions
listed as "adds" were already present in the repository and have only
been added to this reference.
Summary of changes:
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 | 18 +-
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 | 1248 +-
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 | 18 +
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 +-
Help/HYP_TAC.doc | 0
IEEE/fixed_thms.hl | 2 +-
IsabelleLight/README | 71 +-
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 | 4442 ++++++
Library/pocklington.ml | 10 +-
Library/pratt.ml | 4 +-
Library/prime.ml | 63 +-
Library/transc.ml | 233 +-
Makefile | 19 +-
Minisat/minisat_parse.ml | 10 +-
Multivariate/canal.ml | 30 +-
Multivariate/cauchy.ml | 28 +-
Multivariate/complex_database.ml | 1360 +-
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/homology.ml | 3776 +++++
Multivariate/integration.ml | 148 +-
Multivariate/lpspaces.ml | 107 +-
Multivariate/measure.ml | 252 +-
Multivariate/metric.ml | 15025 ++++++++++++++++++-
Multivariate/misc.ml | 949 +-
Multivariate/moretop.ml | 214 +-
Multivariate/multivariate_database.ml | 1344 +-
Multivariate/paths.ml | 983 +-
Multivariate/polytope.ml | 32 +-
Multivariate/realanalysis.ml | 2358 ++-
Multivariate/topology.ml | 5901 +++++---
Multivariate/transcendentals.ml | 134 +-
Multivariate/vectors.ml | 564 +-
Ntrie/ntrie.ml | 1377 +-
Ntrie/ntrie_tests.ml | 181 -
Proofrecording/hol_light/Makefile | 74 +-
Proofrecording/tools/detecteq.jar | Bin 7516 -> 0 bytes
Proofrecording/tools/nametheorems.jar | Bin 2482 -> 0 bytes
Proofrecording/tools/src/Makefile | 13 +
Quaternions/qanal.hl | 4 +-
Quaternions/qnormalizer.hl | 21 +-
.../TarskiAxiomGeometry_read.ml | 0
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 | 197 +-
drule.ml | 4 +-
grobner.ml | 10 +-
holtest | 3 +
holtest.mk | 100 +-
ind_types.ml | 4 +-
int.ml | 54 +-
lists.ml | 39 +-
nums.ml | 8 +-
pa_j_3.1x_6.11.ml => pa_j_4.xx_7.xx.ml | 5 +-
pair.ml | 27 +-
parser.ml | 34 +-
printer.ml | 41 +-
real.ml | 477 +-
sets.ml | 900 +-
tactics.ml | 2 +-
215 files changed, 76323 insertions(+), 28020 deletions(-)
create mode 100644 Formal_ineqs/README.md
delete mode 100644 Formal_ineqs/README.txt
rename Formal_ineqs/arith/{float.hl => arith_float.hl} (61%)
create mode 100644 Formal_ineqs/arith/arith_nat.hl
delete mode 100644 Formal_ineqs/arith/float_atn.hl
create mode 100644 Formal_ineqs/arith/float_pow.hl
delete mode 100644 Formal_ineqs/arith/nat.hl
create mode 100644 Formal_ineqs/examples_other.hl
delete mode 100644 Formal_ineqs/informal/informal_arith.hl
create mode 100644 Formal_ineqs/informal/informal_asn_acs.hl
create mode 100644 Formal_ineqs/informal/informal_atn.hl
create mode 100644 Formal_ineqs/informal/informal_exp.hl
create mode 100644 Formal_ineqs/informal/informal_float.hl
create mode 100644 Formal_ineqs/informal/informal_interval.hl
create mode 100644 Formal_ineqs/informal/informal_log.hl
delete mode 100644 Formal_ineqs/informal/informal_m_taylor.hl
delete mode 100644 Formal_ineqs/informal/informal_m_verifier.hl
create mode 100644 Formal_ineqs/informal/informal_matan.hl
create mode 100644 Formal_ineqs/informal/informal_nat.hl
create mode 100644 Formal_ineqs/informal/informal_poly.hl
create mode 100644 Formal_ineqs/informal/informal_search.hl
create mode 100644 Formal_ineqs/informal/informal_sin_cos.hl
create mode 100644 Formal_ineqs/informal/informal_taylor.hl
create mode 100644 Formal_ineqs/informal/informal_verifier.hl
delete mode 100644 Formal_ineqs/jordan/parse_ext_override_interface.hl
delete mode 100644 Formal_ineqs/jordan/real_ext.hl
delete mode 100644 Formal_ineqs/jordan/refinement.hl
delete mode 100644 Formal_ineqs/jordan/taylor_atn.hl
create mode 100644 Formal_ineqs/lib/ipow.hl
delete mode 100644 Formal_ineqs/lib/ssrbool-compiled.hl
create mode 100644 Formal_ineqs/lib/ssrbool.hl
delete mode 100644 Formal_ineqs/lib/ssrfun-compiled.hl
create mode 100644 Formal_ineqs/lib/ssrfun.hl
delete mode 100644 Formal_ineqs/lib/ssrnat-compiled.hl
create mode 100644 Formal_ineqs/lib/ssrnat.hl
rename Formal_ineqs/misc/{misc.hl => misc_functions.hl} (51%)
rename Formal_ineqs/misc/{vars.hl => misc_vars.hl} (54%)
rename Formal_ineqs/{verifier/interval_m/report.ml => misc/report.hl} (73%)
create mode 100755 Formal_ineqs/tests/data/gen_nat_data.py
create mode 100644 Formal_ineqs/tests/float_data.hl
create mode 100644 Formal_ineqs/tests/log.hl
create mode 100644 Formal_ineqs/tests/nat_test.hl
create mode 100644 Formal_ineqs/tests/results.hl
create mode 100644 Formal_ineqs/tests/test_utils.hl
create mode 100644 Formal_ineqs/trig/asn_acs_eval.hl
create mode 100644 Formal_ineqs/trig/atn.hl
create mode 100644 Formal_ineqs/trig/atn_eval.hl
create mode 100644 Formal_ineqs/trig/cos_bounds_eval.hl
create mode 100644 Formal_ineqs/trig/cos_eval.hl
create mode 100644 Formal_ineqs/trig/exp_eval.hl
create mode 100644 Formal_ineqs/trig/exp_log.hl
create mode 100644 Formal_ineqs/trig/log_eval.hl
create mode 100644 Formal_ineqs/trig/matan.hl
create mode 100644 Formal_ineqs/trig/matan_eval.hl
create mode 100644 Formal_ineqs/trig/poly.hl
create mode 100644 Formal_ineqs/trig/poly_eval.hl
create mode 100644 Formal_ineqs/trig/series.hl
create mode 100644 Formal_ineqs/trig/sin_cos.hl
create mode 100644 Formal_ineqs/trig/sin_eval.hl
create mode 100644 Formal_ineqs/trig/test.hl
create mode 100644 Formal_ineqs/trig/unused.hl
create mode 100644 Formal_ineqs/verifier/certificate.hl
delete mode 100644 Formal_ineqs/verifier/interval_m/interval.ml
delete mode 100644 Formal_ineqs/verifier/interval_m/line_interval.ml
delete mode 100644 Formal_ineqs/verifier/interval_m/recurse.ml
delete mode 100644 Formal_ineqs/verifier/interval_m/recurse0.ml
delete mode 100644 Formal_ineqs/verifier/interval_m/taylor.ml
delete mode 100644 Formal_ineqs/verifier/interval_m/types.ml
delete mode 100644 Formal_ineqs/verifier/interval_m/univariate.ml
delete mode 100644 Formal_ineqs/verifier/interval_m/verifier.ml
mode change 100755 => 100644 Help/HYP_TAC.doc
create mode 100644 Library/frag.ml
create mode 100644 Library/grouptheory.ml
mode change 100755 => 100644 Multivariate/cvectors.ml
create mode 100644 Multivariate/homology.ml
delete mode 100644 Ntrie/ntrie_tests.ml
delete mode 100644 Proofrecording/tools/detecteq.jar
delete mode 100644 Proofrecording/tools/nametheorems.jar
create mode 100644 Proofrecording/tools/src/Makefile
mode change 100755 => 100644 RichterHilbertAxiomGeometry/TarskiAxiomGeometry_read.ml
copy pa_j_3.1x_6.11.ml => pa_j_4.xx_7.xx.ml (99%)
mode change 100644 => 100755
--
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