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 0d4515f9ce415a6b6a9444404e64243abd3a462d
Merge: a5735d4 991870c
Author: Hendrik Tews <hend...@askra.de>
Date: Mon Jan 9 20:52:16 2017 +0100
Merge tag 'upstream/20170109'
Upstream version 20170109
100/bernoulli.ml | 2 +-
100/cayley_hamilton.ml | 7 +-
100/circle.ml | 2 -
100/constructible.ml | 12 +-
100/e_is_transcendental.ml | 4 +-
100/fourier.ml | 1317 +-
100/heron.ml | 2 +-
100/independence.ml | 148 +-
100/liouville.ml | 2 +-
100/minkowski.ml | 3 +-
100/piseries.ml | 2 +-
100/pnt.ml | 9 +-
100/polyhedron.ml | 4 +-
100/ptolemy.ml | 18 +-
100/ramsey.ml | 12 +-
100/reciprocity.ml | 2 +-
100/sqrt.ml | 42 +
Arithmetic/definability.ml | 2 +-
Boyer_Moore/clausal_form.ml | 4 +-
Boyer_Moore/definitions.ml | 12 +-
Boyer_Moore/environment.ml | 6 +-
Boyer_Moore/equalities.ml | 12 +-
Boyer_Moore/generalize.ml | 46 +-
Boyer_Moore/induction.ml | 2 +-
Boyer_Moore/irrelevance.ml | 2 +-
Boyer_Moore/rewrite_rules.ml | 4 +-
Boyer_Moore/support.ml | 4 +-
Boyer_Moore/terms_and_clauses.ml | 5 +-
Boyer_Moore/waterfall.ml | 16 +-
CHANGES | 2579 +-
Complex/complex_grobner.ml | 24 +-
Complex/complexnumbers.ml | 10 +-
Complex/quelim.ml | 4 +-
Examples/brunn_minkowski.ml | 43 +-
Examples/cooper.ml | 32 +-
Examples/dickson.ml | 85 +
Examples/division_algebras.ml | 575 +
Examples/dlo.ml | 6 +-
Examples/gcdrecurrence.ml | 230 +
Examples/harmonicsum.ml | 123 +
Examples/hol88.ml | 12 +-
Examples/holby.ml | 24 +-
Examples/inverse_bug_puzzle_tac.ml | 2 +-
Examples/kb.ml | 22 +-
Examples/lucas_lehmer.ml | 412 +
Examples/misiurewicz.ml | 1296 +
Examples/mizar.ml | 122 +-
Examples/prog.ml | 52 +-
Examples/prover9.ml | 25 +-
Examples/solovay.ml | 2 +-
Examples/sos.ml | 44 +-
Examples/update_database.ml | 8 +-
Formal_ineqs/README.txt | 8 +
Formal_ineqs/arith/arith_cache.hl | 212 +
Formal_ineqs/arith/arith_num.hl | 1448 +
Formal_ineqs/arith/eval_interval.hl | 278 +
Formal_ineqs/arith/float.hl | 3889 ++
Formal_ineqs/arith/float_atn.hl | 582 +
Formal_ineqs/arith/float_theory.hl | 87 +
Formal_ineqs/arith/interval_arith.hl | 59 +
Formal_ineqs/arith/more_float.hl | 491 +
Formal_ineqs/arith/nat.hl | 102 +
Formal_ineqs/arith/num_exp_theory.hl | 251 +
Formal_ineqs/arith_options.hl | 25 +
Formal_ineqs/docs/FormalVerifier.pdf | Bin 0 -> 223139 bytes
Formal_ineqs/docs/FormalVerifier.tex | 419 +
Formal_ineqs/examples.hl | 74 +
Formal_ineqs/examples_flyspeck.hl | 326 +
Formal_ineqs/examples_poly.hl | 141 +
Formal_ineqs/informal/informal_arith.hl | 805 +
Formal_ineqs/informal/informal_eval_interval.hl | 275 +
Formal_ineqs/informal/informal_m_taylor.hl | 403 +
Formal_ineqs/informal/informal_m_verifier.hl | 302 +
.../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/ssrbool-compiled.hl | 759 +
Formal_ineqs/lib/ssreflect/sections.hl | 273 +
Formal_ineqs/lib/ssreflect/ssreflect.hl | 1032 +
Formal_ineqs/lib/ssrfun-compiled.hl | 304 +
Formal_ineqs/lib/ssrnat-compiled.hl | 1634 +
Formal_ineqs/list/list_conversions.hl | 523 +
Formal_ineqs/list/list_float.hl | 202 +
Formal_ineqs/list/more_list.hl | 128 +
Formal_ineqs/make.ml | 83 +
Formal_ineqs/misc/misc.hl | 61 +
Formal_ineqs/misc/vars.hl | 141 +
Formal_ineqs/taylor/m_taylor.hl | 1487 +
Formal_ineqs/taylor/m_taylor_arith.hl | 1604 +
Formal_ineqs/taylor/m_taylor_arith2.hl | 682 +
.../taylor/theory/multivariate_taylor-compiled.hl | 2917 ++
Formal_ineqs/taylor/theory/multivariate_taylor.vhl | 2411 +
.../taylor/theory/taylor_interval-compiled.hl | 2464 +
Formal_ineqs/taylor/theory/taylor_interval.vhl | 2050 +
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/report.ml | 50 +
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 | 1256 +
Formal_ineqs/verifier/m_verifier_build.hl | 201 +
Formal_ineqs/verifier/m_verifier_main.hl | 463 +
Formal_ineqs/verifier_options.hl | 18 +
Functionspaces/L2.ml | 460 +
Functionspaces/README | 9 +
Functionspaces/cfunspace.ml | 2799 ++
Functionspaces/make.ml | 26 +
Functionspaces/utils.ml | 169 +
Help/.joinparsers.doc | 2 +-
Help/.orparser.doc | 6 +-
Help/.pipeparser.doc | 4 +-
Help/ABBREV_TAC.doc | 2 +-
Help/ALPHA_CONV.doc | 10 +-
Help/ARITH_RULE.doc | 2 +-
Help/ASM_MESON_TAC.doc | 2 +-
Help/{ASM_MESON_TAC.doc => ASM_METIS_TAC.doc} | 13 +-
Help/CASE_REWRITE_TAC.doc | 45 +
Help/CHAR_EQ_CONV.doc | 43 +
Help/CLAIM_TAC.doc | 62 +
Help/CONTR.doc | 2 +-
Help/DESTRUCT_TAC.doc | 45 +-
Help/DISCH.doc | 2 +-
Help/DISJ_CASES_THEN.doc | 2 +-
Help/EQ_MP.doc | 15 +-
Help/EXISTS_TAC.doc | 2 +-
Help/FIX_TAC.doc | 32 +-
Help/GEN_MESON_TAC.doc | 14 +-
Help/GEN_PART_MATCH.doc | 2 +-
Help/GEN_REWRITE_TAC.doc | 2 +-
Help/GSYM.doc | 2 +-
Help/HINT_EXISTS_TAC.doc | 51 +
Help/HYP_TAC.doc | 69 +
Help/HYP_UPPERCASE.doc | 2 +-
Help/IMP_REWRITE_TAC.doc | 130 +
Help/INST_UPPERCASE.doc | 6 +-
Help/INTRO_TAC.doc | 35 +-
Help/INT_OF_REAL_THM.doc | 4 +-
Help/LAMBDA_ELIM_CONV.doc | 2 +-
Help/MESON.doc | 9 +-
Help/MESON_TAC.doc | 4 +-
Help/METIS.doc | 40 +
Help/METIS_TAC.doc | 49 +
Help/NUMSEG_CONV.doc | 4 +-
Help/NUM_CANCEL_CONV.doc | 14 +-
Help/NUM_SIMPLIFY_CONV.doc | 6 +-
Help/ORELSEC.doc | 2 +-
Help/PART_MATCH.doc | 2 +-
Help/PAT_CONV.doc | 6 +-
Help/PRESIMP_CONV.doc | 2 +-
Help/PROVE_HYP.doc | 11 +-
Help/REWRITE_CONV.doc | 6 +-
Help/REWRITE_TAC.doc | 7 +-
Help/SEQ_IMP_REWRITE_TAC.doc | 57 +
Help/SIMPLE_DISJ_CASES.doc | 14 +-
Help/SIMP_TAC.doc | 4 +-
Help/SPECL.doc | 2 +-
Help/SPEC_VAR.doc | 2 +-
Help/STRING_EQ_CONV.doc | 37 +
Help/SUBGOAL_TAC.doc | 2 +-
Help/SUBGOAL_THEN.doc | 2 +-
Help/TARGET_REWRITE_TAC.doc | 117 +
Help/TOP_DEPTH_CONV.doc | 2 +-
Help/TRANS.doc | 11 +-
Help/a.doc | 4 +-
Help/atleast.doc | 2 +-
Help/can.doc | 2 +-
Help/dest_char.doc | 32 +
Help/dest_imp.doc | 6 +-
Help/dest_small_numeral.doc | 8 +-
Help/dest_string.doc | 25 +
Help/distinctness.doc | 10 +-
Help/dom.doc | 8 +-
Help/e.doc | 4 +-
Help/elistof.doc | 4 +-
Help/file_of_string.doc | 8 +-
Help/finished.doc | 8 +-
Help/fix.doc | 8 +-
Help/foldl.doc | 4 +-
Help/injectivity.doc | 26 +-
Help/install_user_printer.doc | 11 +-
Help/is_eq.doc | 2 +-
Help/is_hidden.doc | 9 +-
Help/leftbin.doc | 16 +-
Help/listof.doc | 2 +-
Help/many.doc | 8 +-
Help/mk_char.doc | 29 +
Help/mk_comb.doc | 6 +-
Help/mk_fset.doc | 10 +-
Help/mk_string.doc | 27 +
Help/new_type.doc | 9 +-
Help/nothing.doc | 8 +-
Help/possibly.doc | 6 +-
Help/prove_constructors_distinct.doc | 2 +-
Help/r.doc | 22 +-
Help/ran.doc | 8 +-
Help/remark.doc | 6 +-
Help/rightbin.doc | 24 +-
Help/set_goal.doc | 2 +-
Help/some.doc | 2 +-
Help/time.doc | 10 +-
Help/try_user_printer.doc | 19 +-
Help/tysubst.doc | 10 +-
Help/vfree_in.doc | 2 +-
IEEE/README | 34 +
IEEE/common.hl | 768 +
IEEE/fixed.hl | 131 +
IEEE/fixed_thms.hl | 2378 +
IEEE/float.hl | 212 +
IEEE/float_thms.hl | 5621 +++
IEEE/ieee.hl | 174 +
IEEE/ieee_thms.hl | 460 +
IEEE/make.ml | 11 +
IsabelleLight/support.ml | 43 +-
Jordan/float.ml | 14 +-
Jordan/tactics_ext2.ml | 23 +-
LP_arith/lp_arith.ml | 2 +-
Library/analysis.ml | 6 +-
Library/binary.ml | 4 -
Library/binomial.ml | 80 +-
Library/calc_real.ml | 6 +-
Library/card.ml | 1027 +-
Library/floor.ml | 133 +-
Library/integer.ml | 18 +-
Library/isum.ml | 5 +
Library/iter.ml | 114 +
Library/permutations.ml | 109 +-
Library/pocklington.ml | 143 +-
Library/prime.ml | 580 +-
Library/primitive.ml | 2 +-
Library/products.ml | 362 +-
Library/q.ml | 153 +
Library/wo.ml | 452 +-
Makefile | 37 +-
Minisat/README | 2 +-
Minisat/minisat_parse.ml | 2 +-
Minisat/minisat_prove.ml | 10 +-
Minisat/sat_tools.ml | 2 +-
Minisat/taut.ml | 2 +-
Minisat/zc2mso/zc2mso.C | 1 +
Multivariate/canal.ml | 875 +-
Multivariate/cauchy.ml | 6514 ++-
Multivariate/clifford.ml | 2 +-
Multivariate/complex_database.ml | 4170 +-
Multivariate/complexes.ml | 455 +-
Multivariate/convex.ml | 8383 +++-
Multivariate/cvectors.ml | 2032 +
Multivariate/degree.ml | 11934 +++++
Multivariate/derivatives.ml | 3324 +-
Multivariate/determinants.ml | 1638 +-
Multivariate/dimension.ml | 5861 ---
Multivariate/flyspeck.ml | 68 +-
Multivariate/gamma.ml | 3778 ++
Multivariate/geom.ml | 316 +
Multivariate/integration.ml | 31941 +++++++-----
Multivariate/lpspaces.ml | 1212 +
Multivariate/make.ml | 13 +-
Multivariate/make_complex.ml | 16 +-
Multivariate/measure.ml | 22074 ++++++++-
Multivariate/metric.ml | 3928 ++
Multivariate/misc.ml | 1494 +-
Multivariate/moretop.ml | 1681 +-
Multivariate/multivariate_database.ml | 3727 +-
Multivariate/paths.ml | 16923 +++++--
Multivariate/polytope.ml | 3494 +-
Multivariate/realanalysis.ml | 4051 +-
Multivariate/topology.ml | 49517 +++++++++++++------
Multivariate/transcendentals.ml | 1882 +-
Multivariate/vectors.ml | 2654 +-
Permutation/morelist.ml | 17 +
Permutation/permutation.ml | 7 +
Permutation/permuted.ml | 17 +
Permutation/qsort.ml | 6 +
Proofrecording/diffs/basics.ml | 8 +-
Proofrecording/diffs/equal.ml | 2 +-
Proofrecording/diffs/proofobjects_coq.ml | 2 +-
Proofrecording/diffs/proofobjects_trt.ml | 2 +-
Proofrecording/diffs/tactics.ml | 12 +-
Proofrecording/diffs/thm.ml | 6 +-
Quaternions/COPYING | 26 +
Quaternions/make.ml | 18 +
Quaternions/misc.hl | 72 +
Quaternions/qanal.hl | 492 +
Quaternions/qcalc.hl | 182 +
Quaternions/qderivative.hl | 63 +
Quaternions/qisom.hl | 316 +
Quaternions/qnormalizer.hl | 346 +
Quaternions/quaternion.hl | 1295 +
README | 55 +-
RichterHilbertAxiomGeometry/HilbertAxiom_read.ml | 1804 +-
RichterHilbertAxiomGeometry/README | 41 +-
.../TarskiAxiomGeometry_read.ml | 659 +
RichterHilbertAxiomGeometry/Topology.ml | 3548 +-
.../UniversalPropCartProd.ml | 19 +-
RichterHilbertAxiomGeometry/error-checking.ml | 44 +-
.../from_topology.ml | 4564 +-
.../inverse_bug_puzzle_read.ml | 11 +-
.../miz3/hol-light-fonts.el | 39 +-
.../miz3/hol-light-fonts.elc | Bin 9289 -> 9857 bytes
RichterHilbertAxiomGeometry/readable.ml | 250 +-
RichterHilbertAxiomGeometry/thmFontHilbertAxiom | 976 +
RichterHilbertAxiomGeometry/thmTopology | 1685 +
Rqe/condense.ml | 2 +-
Rqe/defs.ml | 2 +-
Rqe/lift_qelim.ml | 4 +-
Rqe/pdivides.ml | 6 +-
Rqe/poly_ext.ml | 12 +-
Rqe/rqe_lib.ml | 2 +-
Rqe/rqe_main.ml | 20 +-
Rqe/signs.ml | 18 +-
Rqe/simplify.ml | 10 +-
Rqe/testform.ml | 2 +-
Rqe/testform_thms.ml | 10 +-
Tutorial/Custom_inference_rules.ml | 22 +-
Tutorial/Custom_tactics.ml | 8 +-
Tutorial/Linking_external_tools.ml | 2 +-
Tutorial/all.ml | 32 +-
arith.ml | 55 +
basics.ml | 12 +-
bool.ml | 53 +-
calc_int.ml | 8 +-
calc_num.ml | 1416 +-
calc_rat.ml | 54 +-
canon.ml | 30 +-
cart.ml | 82 +
class.ml | 17 +-
database.ml | 194 +
define.ml | 14 +-
drule.ml | 18 +-
equal.ml | 46 +-
fusion.ml | 27 +-
grobner.ml | 50 +-
help.ml | 8 +-
hol.ml | 4 +-
holtest | 33 +-
holtest.mk | 218 +
holtest_parallel | 42 +
impconv.ml | 1856 +
ind_defs.ml | 25 +-
ind_types.ml | 22 +-
int.ml | 46 +-
iterate.ml | 463 +-
lib.ml | 16 +-
lists.ml | 206 +-
meson.ml | 190 +-
metis.ml | 10162 ++++
miz3/miz3.ml | 80 +-
miz3/miz3_of_hol.ml | 10 +-
normalizer.ml | 22 +-
nums.ml | 60 +-
pa_j_3.1x_6.11.ml | 14 +-
pair.ml | 33 +-
parser.ml | 142 +-
preterm.ml | 16 +-
printer.ml | 77 +-
real.ml | 60 +
realarith.ml | 10 +-
realax.ml | 4 +-
sets.ml | 824 +-
simp.ml | 16 +-
system.ml | 9 +-
tactics.ml | 10 +-
term.ml | 276 -
theorems.ml | 150 +-
thm.ml | 243 -
type.ml | 143 -
update_database.ml | 8 +-
wf.ml | 34 +-
372 files changed, 239412 insertions(+), 48365 deletions(-)
--
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
