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  fc867d4   Imported Upstream version 20131026
       new  991870c   Imported Upstream version 20170109

The 1 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/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(-)
 create mode 100644 100/sqrt.ml
 create mode 100644 Examples/dickson.ml
 create mode 100644 Examples/division_algebras.ml
 create mode 100644 Examples/gcdrecurrence.ml
 create mode 100644 Examples/harmonicsum.ml
 create mode 100644 Examples/lucas_lehmer.ml
 create mode 100644 Examples/misiurewicz.ml
 create mode 100644 Formal_ineqs/README.txt
 create mode 100644 Formal_ineqs/arith/arith_cache.hl
 create mode 100644 Formal_ineqs/arith/arith_num.hl
 create mode 100644 Formal_ineqs/arith/eval_interval.hl
 create mode 100644 Formal_ineqs/arith/float.hl
 create mode 100644 Formal_ineqs/arith/float_atn.hl
 create mode 100644 Formal_ineqs/arith/float_theory.hl
 create mode 100644 Formal_ineqs/arith/interval_arith.hl
 create mode 100644 Formal_ineqs/arith/more_float.hl
 create mode 100644 Formal_ineqs/arith/nat.hl
 create mode 100644 Formal_ineqs/arith/num_exp_theory.hl
 create mode 100644 Formal_ineqs/arith_options.hl
 create mode 100644 Formal_ineqs/docs/FormalVerifier.pdf
 create mode 100644 Formal_ineqs/docs/FormalVerifier.tex
 create mode 100644 Formal_ineqs/examples.hl
 create mode 100644 Formal_ineqs/examples_flyspeck.hl
 create mode 100644 Formal_ineqs/examples_poly.hl
 create mode 100644 Formal_ineqs/informal/informal_arith.hl
 create mode 100644 Formal_ineqs/informal/informal_eval_interval.hl
 create mode 100644 Formal_ineqs/informal/informal_m_taylor.hl
 create mode 100644 Formal_ineqs/informal/informal_m_verifier.hl
 create mode 100644 Formal_ineqs/jordan/parse_ext_override_interface.hl
 create mode 100644 Formal_ineqs/jordan/real_ext.hl
 create mode 100644 Formal_ineqs/jordan/refinement.hl
 create mode 100644 Formal_ineqs/jordan/taylor_atn.hl
 create mode 100644 Formal_ineqs/lib/ssrbool-compiled.hl
 create mode 100644 Formal_ineqs/lib/ssreflect/sections.hl
 create mode 100644 Formal_ineqs/lib/ssreflect/ssreflect.hl
 create mode 100644 Formal_ineqs/lib/ssrfun-compiled.hl
 create mode 100644 Formal_ineqs/lib/ssrnat-compiled.hl
 create mode 100644 Formal_ineqs/list/list_conversions.hl
 create mode 100644 Formal_ineqs/list/list_float.hl
 create mode 100644 Formal_ineqs/list/more_list.hl
 create mode 100644 Formal_ineqs/make.ml
 create mode 100644 Formal_ineqs/misc/misc.hl
 create mode 100644 Formal_ineqs/misc/vars.hl
 create mode 100644 Formal_ineqs/taylor/m_taylor.hl
 create mode 100644 Formal_ineqs/taylor/m_taylor_arith.hl
 create mode 100644 Formal_ineqs/taylor/m_taylor_arith2.hl
 create mode 100644 Formal_ineqs/taylor/theory/multivariate_taylor-compiled.hl
 create mode 100644 Formal_ineqs/taylor/theory/multivariate_taylor.vhl
 create mode 100644 Formal_ineqs/taylor/theory/taylor_interval-compiled.hl
 create mode 100644 Formal_ineqs/taylor/theory/taylor_interval.vhl
 create mode 100644 Formal_ineqs/verifier/interval_m/interval.ml
 create mode 100644 Formal_ineqs/verifier/interval_m/line_interval.ml
 create mode 100644 Formal_ineqs/verifier/interval_m/recurse.ml
 create mode 100644 Formal_ineqs/verifier/interval_m/recurse0.ml
 create mode 100644 Formal_ineqs/verifier/interval_m/report.ml
 create mode 100644 Formal_ineqs/verifier/interval_m/taylor.ml
 create mode 100644 Formal_ineqs/verifier/interval_m/types.ml
 create mode 100644 Formal_ineqs/verifier/interval_m/univariate.ml
 create mode 100644 Formal_ineqs/verifier/interval_m/verifier.ml
 create mode 100644 Formal_ineqs/verifier/m_verifier.hl
 create mode 100644 Formal_ineqs/verifier/m_verifier_build.hl
 create mode 100644 Formal_ineqs/verifier/m_verifier_main.hl
 create mode 100644 Formal_ineqs/verifier_options.hl
 create mode 100644 Functionspaces/L2.ml
 create mode 100644 Functionspaces/README
 create mode 100644 Functionspaces/cfunspace.ml
 create mode 100644 Functionspaces/make.ml
 create mode 100644 Functionspaces/utils.ml
 copy Help/{ASM_MESON_TAC.doc => ASM_METIS_TAC.doc} (53%)
 create mode 100644 Help/CASE_REWRITE_TAC.doc
 create mode 100644 Help/CHAR_EQ_CONV.doc
 create mode 100644 Help/CLAIM_TAC.doc
 create mode 100644 Help/HINT_EXISTS_TAC.doc
 create mode 100755 Help/HYP_TAC.doc
 create mode 100644 Help/IMP_REWRITE_TAC.doc
 create mode 100644 Help/METIS.doc
 create mode 100644 Help/METIS_TAC.doc
 create mode 100644 Help/SEQ_IMP_REWRITE_TAC.doc
 create mode 100644 Help/STRING_EQ_CONV.doc
 create mode 100644 Help/TARGET_REWRITE_TAC.doc
 create mode 100644 Help/dest_char.doc
 create mode 100644 Help/dest_string.doc
 create mode 100644 Help/mk_char.doc
 create mode 100644 Help/mk_string.doc
 create mode 100644 IEEE/README
 create mode 100644 IEEE/common.hl
 create mode 100644 IEEE/fixed.hl
 create mode 100644 IEEE/fixed_thms.hl
 create mode 100644 IEEE/float.hl
 create mode 100644 IEEE/float_thms.hl
 create mode 100644 IEEE/ieee.hl
 create mode 100644 IEEE/ieee_thms.hl
 create mode 100644 IEEE/make.ml
 create mode 100644 Library/q.ml
 create mode 100755 Multivariate/cvectors.ml
 create mode 100644 Multivariate/degree.ml
 delete mode 100644 Multivariate/dimension.ml
 create mode 100644 Multivariate/gamma.ml
 create mode 100644 Multivariate/lpspaces.ml
 create mode 100644 Multivariate/metric.ml
 create mode 100644 Quaternions/COPYING
 create mode 100644 Quaternions/make.ml
 create mode 100644 Quaternions/misc.hl
 create mode 100644 Quaternions/qanal.hl
 create mode 100644 Quaternions/qcalc.hl
 create mode 100644 Quaternions/qderivative.hl
 create mode 100644 Quaternions/qisom.hl
 create mode 100644 Quaternions/qnormalizer.hl
 create mode 100644 Quaternions/quaternion.hl
 create mode 100755 RichterHilbertAxiomGeometry/TarskiAxiomGeometry_read.ml
 mode change 100755 => 100644 RichterHilbertAxiomGeometry/Topology.ml
 copy Multivariate/topology.ml => RichterHilbertAxiomGeometry/from_topology.ml 
(88%)
 create mode 100644 RichterHilbertAxiomGeometry/thmFontHilbertAxiom
 create mode 100644 RichterHilbertAxiomGeometry/thmTopology
 create mode 100644 holtest.mk
 create mode 100755 holtest_parallel
 create mode 100644 impconv.ml
 create mode 100644 metis.ml
 delete mode 100644 term.ml
 delete mode 100644 thm.ml
 delete mode 100644 type.ml

-- 
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

Reply via email to