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 _______________________________________________ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits