hol-light_20170109-1_amd64.deb


Advertisement

Description

hol-light - HOL Light theorem prover

Property Value
Distribution Debian 9 (Stretch)
Repository Debian Main amd64
Package name hol-light
Package version 20170109
Package release 1
Package architecture amd64
Package type deb
Installed size 31.36 KB
Download size 4.09 MB
Official Mirror ftp.br.debian.org
HOL Light is an interactive theorem prover for Higher-Order Logic
with a very simple logical core running in an OCaml toplevel. HOL
Light is famous for the verification of floating-point
arithmetic as well as for the Flyspeck project, which aims at the
formalization of Tom Hales' proof of the Kepler conjecture.

Alternatives

Package Version Architecture Repository
hol-light_20170109-1_i386.deb 20170109 i386 Debian Main
hol-light - - -

Requires

Name Value
camlp5 -
camlp5-ixut4 -
ocaml-nox-4.02.3 -

Download

Type URL
Binary Package hol-light_20170109-1_amd64.deb
Source Package hol-light

Install Howto

  1. Update the package index:
    # sudo apt-get update
  2. Install hol-light deb package:
    # sudo apt-get install hol-light

Files

Path
/usr/bin/hol-light
/usr/share/doc/hol-light/QUICK_REFERENCE.txt.gz
/usr/share/doc/hol-light/README.Debian
/usr/share/doc/hol-light/README.gz
/usr/share/doc/hol-light/VERYQUICK_REFERENCE.txt.gz
/usr/share/doc/hol-light/changelog.Debian.gz
/usr/share/doc/hol-light/changelog.gz
/usr/share/doc/hol-light/copyright
/usr/share/hol-light/arith.ml
/usr/share/hol-light/basics.ml
/usr/share/hol-light/bool.ml
/usr/share/hol-light/calc_int.ml
/usr/share/hol-light/calc_num.ml
/usr/share/hol-light/calc_rat.ml
/usr/share/hol-light/canon.ml
/usr/share/hol-light/cart.ml
/usr/share/hol-light/class.ml
/usr/share/hol-light/database.ml
/usr/share/hol-light/define.ml
/usr/share/hol-light/doc-to-help.sed
/usr/share/hol-light/drule.ml
/usr/share/hol-light/equal.ml
/usr/share/hol-light/fusion.ml
/usr/share/hol-light/grobner.ml
/usr/share/hol-light/help.ml
/usr/share/hol-light/hol.ml
/usr/share/hol-light/holtest
/usr/share/hol-light/holtest.mk
/usr/share/hol-light/holtest_parallel
/usr/share/hol-light/impconv.ml
/usr/share/hol-light/ind_defs.ml
/usr/share/hol-light/ind_types.ml
/usr/share/hol-light/int.ml
/usr/share/hol-light/itab.ml
/usr/share/hol-light/iterate.ml
/usr/share/hol-light/lib.ml
/usr/share/hol-light/lists.ml
/usr/share/hol-light/make.ml
/usr/share/hol-light/meson.ml
/usr/share/hol-light/metis.ml
/usr/share/hol-light/nets.ml
/usr/share/hol-light/normalizer.ml
/usr/share/hol-light/nums.ml
/usr/share/hol-light/ocamlinit-stamp
/usr/share/hol-light/pa_j.cmi
/usr/share/hol-light/pa_j.cmo
/usr/share/hol-light/pair.ml
/usr/share/hol-light/parser.ml
/usr/share/hol-light/preterm.ml
/usr/share/hol-light/printer.ml
/usr/share/hol-light/quot.ml
/usr/share/hol-light/real.ml
/usr/share/hol-light/realarith.ml
/usr/share/hol-light/realax.ml
/usr/share/hol-light/recursion.ml
/usr/share/hol-light/sets.ml
/usr/share/hol-light/simp.ml
/usr/share/hol-light/system.ml
/usr/share/hol-light/tactics.ml
/usr/share/hol-light/theorems.ml
/usr/share/hol-light/trivia.ml
/usr/share/hol-light/update_database.ml
/usr/share/hol-light/wf.ml
/usr/share/hol-light/.pc/.quilt_patches
/usr/share/hol-light/.pc/.quilt_series
/usr/share/hol-light/.pc/.version
/usr/share/hol-light/.pc/applied-patches
/usr/share/hol-light/.pc/cd-holtest-parallel.patch/holtest_parallel
/usr/share/hol-light/.pc/default-hollight-dir/hol.ml
/usr/share/hol-light/.pc/holtest-no-proof-recording.patch/holtest
/usr/share/hol-light/100/arithmetic.ml
/usr/share/hol-light/100/arithmetic_geometric_mean.ml
/usr/share/hol-light/100/ballot.ml
/usr/share/hol-light/100/bernoulli.ml
/usr/share/hol-light/100/bertrand.ml
/usr/share/hol-light/100/birthday.ml
/usr/share/hol-light/100/cantor.ml
/usr/share/hol-light/100/cayley_hamilton.ml
/usr/share/hol-light/100/ceva.ml
/usr/share/hol-light/100/chords.ml
/usr/share/hol-light/100/circle.ml
/usr/share/hol-light/100/combinations.ml
/usr/share/hol-light/100/constructible.ml
/usr/share/hol-light/100/cosine.ml
/usr/share/hol-light/100/cubic.ml
/usr/share/hol-light/100/derangements.ml
/usr/share/hol-light/100/desargues.ml
/usr/share/hol-light/100/descartes.ml
/usr/share/hol-light/100/dirichlet.ml
/usr/share/hol-light/100/div3.ml
/usr/share/hol-light/100/divharmonic.ml
/usr/share/hol-light/100/e_is_transcendental.ml
/usr/share/hol-light/100/euler.ml
/usr/share/hol-light/100/feuerbach.ml
/usr/share/hol-light/100/four_squares.ml
/usr/share/hol-light/100/fourier.ml
/usr/share/hol-light/100/friendship.ml
/usr/share/hol-light/100/fta.ml
/usr/share/hol-light/100/gcd.ml
/usr/share/hol-light/100/heron.ml
/usr/share/hol-light/100/inclusion_exclusion.ml
/usr/share/hol-light/100/independence.ml
/usr/share/hol-light/100/isosceles.ml
/usr/share/hol-light/100/konigsberg.ml
/usr/share/hol-light/100/lagrange.ml
/usr/share/hol-light/100/leibniz.ml
/usr/share/hol-light/100/lhopital.ml
/usr/share/hol-light/100/liouville.ml
/usr/share/hol-light/100/minkowski.ml
/usr/share/hol-light/100/morley.ml
/usr/share/hol-light/100/pascal.ml
/usr/share/hol-light/100/perfect.ml
/usr/share/hol-light/100/pick.ml
/usr/share/hol-light/100/piseries.ml
/usr/share/hol-light/100/platonic.ml
/usr/share/hol-light/100/pnt.ml
/usr/share/hol-light/100/polyhedron.ml
/usr/share/hol-light/100/primerecip.ml
/usr/share/hol-light/100/ptolemy.ml
/usr/share/hol-light/100/pythagoras.ml
/usr/share/hol-light/100/quartic.ml
/usr/share/hol-light/100/ramsey.ml
/usr/share/hol-light/100/ratcountable.ml
/usr/share/hol-light/100/realsuncountable.ml
/usr/share/hol-light/100/reciprocity.ml
/usr/share/hol-light/100/sqrt.ml
/usr/share/hol-light/100/stirling.ml
/usr/share/hol-light/100/subsequence.ml
/usr/share/hol-light/100/thales.ml
/usr/share/hol-light/100/triangular.ml
/usr/share/hol-light/100/two_squares.ml
/usr/share/hol-light/100/wilson.ml
/usr/share/hol-light/Arithmetic/arithprov.ml
/usr/share/hol-light/Arithmetic/definability.ml
/usr/share/hol-light/Arithmetic/derived.ml
/usr/share/hol-light/Arithmetic/fol.ml
/usr/share/hol-light/Arithmetic/godel.ml
/usr/share/hol-light/Arithmetic/make.ml
/usr/share/hol-light/Arithmetic/pa.ml
/usr/share/hol-light/Arithmetic/sigmacomplete.ml
/usr/share/hol-light/Arithmetic/tarski.ml
/usr/share/hol-light/Boyer_Moore/README
/usr/share/hol-light/Boyer_Moore/boyer-moore.ml
/usr/share/hol-light/Boyer_Moore/clausal_form.ml
/usr/share/hol-light/Boyer_Moore/counterexample.ml
/usr/share/hol-light/Boyer_Moore/definitions.ml
/usr/share/hol-light/Boyer_Moore/environment.ml
/usr/share/hol-light/Boyer_Moore/equalities.ml
/usr/share/hol-light/Boyer_Moore/generalize.ml
/usr/share/hol-light/Boyer_Moore/induction.ml
/usr/share/hol-light/Boyer_Moore/irrelevance.ml
/usr/share/hol-light/Boyer_Moore/main.ml
/usr/share/hol-light/Boyer_Moore/make.ml
/usr/share/hol-light/Boyer_Moore/rewrite_rules.ml
/usr/share/hol-light/Boyer_Moore/shells.ml
/usr/share/hol-light/Boyer_Moore/struct_equal.ml
/usr/share/hol-light/Boyer_Moore/support.ml
/usr/share/hol-light/Boyer_Moore/terms_and_clauses.ml
/usr/share/hol-light/Boyer_Moore/waterfall.ml
/usr/share/hol-light/Boyer_Moore/testset/arith.ml
/usr/share/hol-light/Boyer_Moore/testset/list.ml
/usr/share/hol-light/Boyer_Moore/testset/res1.pdf
/usr/share/hol-light/Boyer_Moore/testset/res2.pdf
/usr/share/hol-light/Complex/complex_grobner.ml
/usr/share/hol-light/Complex/complex_real.ml
/usr/share/hol-light/Complex/complex_transc.ml
/usr/share/hol-light/Complex/complexnumbers.ml
/usr/share/hol-light/Complex/cpoly.ml
/usr/share/hol-light/Complex/fundamental.ml
/usr/share/hol-light/Complex/grobner_examples.ml
/usr/share/hol-light/Complex/make.ml
/usr/share/hol-light/Complex/quelim.ml
/usr/share/hol-light/Complex/quelim_examples.ml
/usr/share/hol-light/Examples/borsuk.ml
/usr/share/hol-light/Examples/brunn_minkowski.ml
/usr/share/hol-light/Examples/combin.ml
/usr/share/hol-light/Examples/cong.ml
/usr/share/hol-light/Examples/cooper.ml
/usr/share/hol-light/Examples/dickson.ml
/usr/share/hol-light/Examples/division_algebras.ml
/usr/share/hol-light/Examples/dlo.ml
/usr/share/hol-light/Examples/forster.ml
/usr/share/hol-light/Examples/gcdrecurrence.ml
/usr/share/hol-light/Examples/harmonicsum.ml
/usr/share/hol-light/Examples/hol88.ml
/usr/share/hol-light/Examples/holby.ml
/usr/share/hol-light/Examples/inverse_bug_puzzle_miz3.ml
/usr/share/hol-light/Examples/inverse_bug_puzzle_tac.ml
/usr/share/hol-light/Examples/kb.ml
/usr/share/hol-light/Examples/lagrange_lemma.ml
/usr/share/hol-light/Examples/lucas_lehmer.ml
/usr/share/hol-light/Examples/machin.ml
/usr/share/hol-light/Examples/mangoldt.ml
/usr/share/hol-light/Examples/mccarthy.ml
/usr/share/hol-light/Examples/misiurewicz.ml
/usr/share/hol-light/Examples/mizar.ml
/usr/share/hol-light/Examples/multiwf.ml
/usr/share/hol-light/Examples/pell.ml
/usr/share/hol-light/Examples/polylog.ml
/usr/share/hol-light/Examples/prog.ml
/usr/share/hol-light/Examples/prover9.ml
/usr/share/hol-light/Examples/rectypes.ml
/usr/share/hol-light/Examples/reduct.ml
/usr/share/hol-light/Examples/schnirelmann.ml
/usr/share/hol-light/Examples/solovay.ml
/usr/share/hol-light/Examples/sos.ml
/usr/share/hol-light/Examples/ste.ml
/usr/share/hol-light/Examples/sylvester_gallai.ml
/usr/share/hol-light/Examples/update_database.ml
/usr/share/hol-light/Examples/vitali.ml
/usr/share/hol-light/Formal_ineqs/README.txt
/usr/share/hol-light/Formal_ineqs/arith_options.hl
/usr/share/hol-light/Formal_ineqs/examples.hl
/usr/share/hol-light/Formal_ineqs/examples_flyspeck.hl
/usr/share/hol-light/Formal_ineqs/examples_poly.hl
/usr/share/hol-light/Formal_ineqs/make.ml
/usr/share/hol-light/Formal_ineqs/verifier_options.hl
/usr/share/hol-light/Formal_ineqs/arith/arith_cache.hl
/usr/share/hol-light/Formal_ineqs/arith/arith_num.hl
/usr/share/hol-light/Formal_ineqs/arith/eval_interval.hl
/usr/share/hol-light/Formal_ineqs/arith/float.hl
/usr/share/hol-light/Formal_ineqs/arith/float_atn.hl
/usr/share/hol-light/Formal_ineqs/arith/float_theory.hl
/usr/share/hol-light/Formal_ineqs/arith/interval_arith.hl
/usr/share/hol-light/Formal_ineqs/arith/more_float.hl
/usr/share/hol-light/Formal_ineqs/arith/nat.hl
/usr/share/hol-light/Formal_ineqs/arith/num_exp_theory.hl
/usr/share/hol-light/Formal_ineqs/docs/FormalVerifier.pdf
/usr/share/hol-light/Formal_ineqs/docs/FormalVerifier.tex
/usr/share/hol-light/Formal_ineqs/informal/informal_arith.hl
/usr/share/hol-light/Formal_ineqs/informal/informal_eval_interval.hl
/usr/share/hol-light/Formal_ineqs/informal/informal_m_taylor.hl
/usr/share/hol-light/Formal_ineqs/informal/informal_m_verifier.hl
/usr/share/hol-light/Formal_ineqs/jordan/parse_ext_override_interface.hl
/usr/share/hol-light/Formal_ineqs/jordan/real_ext.hl
/usr/share/hol-light/Formal_ineqs/jordan/refinement.hl
/usr/share/hol-light/Formal_ineqs/jordan/taylor_atn.hl
/usr/share/hol-light/Formal_ineqs/lib/ssrbool-compiled.hl
/usr/share/hol-light/Formal_ineqs/lib/ssrfun-compiled.hl
/usr/share/hol-light/Formal_ineqs/lib/ssrnat-compiled.hl
/usr/share/hol-light/Formal_ineqs/lib/ssreflect/sections.hl
/usr/share/hol-light/Formal_ineqs/lib/ssreflect/ssreflect.hl
/usr/share/hol-light/Formal_ineqs/list/list_conversions.hl
/usr/share/hol-light/Formal_ineqs/list/list_float.hl
/usr/share/hol-light/Formal_ineqs/list/more_list.hl
/usr/share/hol-light/Formal_ineqs/misc/misc.hl
/usr/share/hol-light/Formal_ineqs/misc/vars.hl
/usr/share/hol-light/Formal_ineqs/taylor/m_taylor.hl
/usr/share/hol-light/Formal_ineqs/taylor/m_taylor_arith.hl
/usr/share/hol-light/Formal_ineqs/taylor/m_taylor_arith2.hl
/usr/share/hol-light/Formal_ineqs/taylor/theory/multivariate_taylor-compiled.hl
/usr/share/hol-light/Formal_ineqs/taylor/theory/multivariate_taylor.vhl
/usr/share/hol-light/Formal_ineqs/taylor/theory/taylor_interval-compiled.hl
/usr/share/hol-light/Formal_ineqs/taylor/theory/taylor_interval.vhl
/usr/share/hol-light/Formal_ineqs/verifier/m_verifier.hl
/usr/share/hol-light/Formal_ineqs/verifier/m_verifier_build.hl
/usr/share/hol-light/Formal_ineqs/verifier/m_verifier_main.hl
/usr/share/hol-light/Formal_ineqs/verifier/interval_m/interval.ml
/usr/share/hol-light/Formal_ineqs/verifier/interval_m/line_interval.ml
/usr/share/hol-light/Formal_ineqs/verifier/interval_m/recurse.ml
/usr/share/hol-light/Formal_ineqs/verifier/interval_m/recurse0.ml
/usr/share/hol-light/Formal_ineqs/verifier/interval_m/report.ml
/usr/share/hol-light/Formal_ineqs/verifier/interval_m/taylor.ml
/usr/share/hol-light/Formal_ineqs/verifier/interval_m/types.ml
/usr/share/hol-light/Formal_ineqs/verifier/interval_m/univariate.ml
/usr/share/hol-light/Formal_ineqs/verifier/interval_m/verifier.ml
/usr/share/hol-light/Functionspaces/L2.ml
/usr/share/hol-light/Functionspaces/README
/usr/share/hol-light/Functionspaces/cfunspace.ml
/usr/share/hol-light/Functionspaces/make.ml
/usr/share/hol-light/Functionspaces/utils.ml
/usr/share/hol-light/Help/.joinparsers.doc
/usr/share/hol-light/Help/.orparser.doc
/usr/share/hol-light/Help/.pipeparser.doc
/usr/share/hol-light/Help/.singlefun.doc
/usr/share/hol-light/Help/.upto.doc
/usr/share/hol-light/Help/.valmod.doc
/usr/share/hol-light/Help/ABBREV_TAC.doc
/usr/share/hol-light/Help/ABS.doc
/usr/share/hol-light/Help/ABS_CONV.doc
/usr/share/hol-light/Help/ABS_TAC.doc
/usr/share/hol-light/Help/AC.doc
/usr/share/hol-light/Help/ACCEPT_TAC.doc
/usr/share/hol-light/Help/ADD_ASSUM.doc
/usr/share/hol-light/Help/ALL_CONV.doc
/usr/share/hol-light/Help/ALL_TAC.doc
/usr/share/hol-light/Help/ALL_THEN.doc
/usr/share/hol-light/Help/ALPHA_CONV.doc
/usr/share/hol-light/Help/ALPHA_UPPERCASE.doc
/usr/share/hol-light/Help/ANTE_RES_THEN.doc
/usr/share/hol-light/Help/ANTS_TAC.doc
/usr/share/hol-light/Help/AP_TERM.doc
/usr/share/hol-light/Help/AP_TERM_TAC.doc
/usr/share/hol-light/Help/AP_THM.doc
/usr/share/hol-light/Help/AP_THM_TAC.doc
/usr/share/hol-light/Help/ARITH_RULE.doc
/usr/share/hol-light/Help/ARITH_TAC.doc
/usr/share/hol-light/Help/ASM.doc
/usr/share/hol-light/Help/ASM_ARITH_TAC.doc
/usr/share/hol-light/Help/ASM_CASES_TAC.doc
/usr/share/hol-light/Help/ASM_FOL_TAC.doc
/usr/share/hol-light/Help/ASM_INT_ARITH_TAC.doc
/usr/share/hol-light/Help/ASM_MESON_TAC.doc
/usr/share/hol-light/Help/ASM_METIS_TAC.doc
/usr/share/hol-light/Help/ASM_REAL_ARITH_TAC.doc
/usr/share/hol-light/Help/ASM_REWRITE_RULE.doc
/usr/share/hol-light/Help/ASM_REWRITE_TAC.doc
/usr/share/hol-light/Help/ASM_SIMP_TAC.doc
/usr/share/hol-light/Help/ASSOC_CONV.doc
/usr/share/hol-light/Help/ASSUME.doc
/usr/share/hol-light/Help/ASSUME_TAC.doc
/usr/share/hol-light/Help/ASSUM_LIST.doc
/usr/share/hol-light/Help/AUGMENT_SIMPSET.doc
/usr/share/hol-light/Help/BETA.doc
/usr/share/hol-light/Help/BETAS_CONV.doc
/usr/share/hol-light/Help/BETA_CONV.doc
/usr/share/hol-light/Help/BETA_RULE.doc
/usr/share/hol-light/Help/BETA_TAC.doc
/usr/share/hol-light/Help/BINDER_CONV.doc
/usr/share/hol-light/Help/BINOP_CONV.doc
/usr/share/hol-light/Help/BINOP_TAC.doc
/usr/share/hol-light/Help/BOOL_CASES_TAC.doc
/usr/share/hol-light/Help/C.doc
/usr/share/hol-light/Help/CACHE_CONV.doc
/usr/share/hol-light/Help/CASE_REWRITE_TAC.doc
/usr/share/hol-light/Help/CCONTR.doc
/usr/share/hol-light/Help/CHANGED_CONV.doc
/usr/share/hol-light/Help/CHANGED_TAC.doc
/usr/share/hol-light/Help/CHAR_EQ_CONV.doc
/usr/share/hol-light/Help/CHEAT_TAC.doc
/usr/share/hol-light/Help/CHOOSE_TAC.doc
/usr/share/hol-light/Help/CHOOSE_THEN.doc
/usr/share/hol-light/Help/CHOOSE_UPPERCASE.doc
/usr/share/hol-light/Help/CLAIM_TAC.doc
/usr/share/hol-light/Help/CNF_CONV.doc
/usr/share/hol-light/Help/COMB2_CONV.doc
/usr/share/hol-light/Help/COMB_CONV.doc
/usr/share/hol-light/Help/CONDS_CELIM_CONV.doc
/usr/share/hol-light/Help/CONDS_ELIM_CONV.doc
/usr/share/hol-light/Help/COND_CASES_TAC.doc
/usr/share/hol-light/Help/COND_ELIM_CONV.doc
/usr/share/hol-light/Help/CONJ.doc
/usr/share/hol-light/Help/CONJUNCT1.doc
/usr/share/hol-light/Help/CONJUNCT2.doc
/usr/share/hol-light/Help/CONJUNCTS_THEN.doc
/usr/share/hol-light/Help/CONJUNCTS_THEN2.doc
/usr/share/hol-light/Help/CONJUNCTS_UPPERCASE.doc
/usr/share/hol-light/Help/CONJ_ACI_RULE.doc
/usr/share/hol-light/Help/CONJ_CANON_CONV.doc
/usr/share/hol-light/Help/CONJ_PAIR.doc
/usr/share/hol-light/Help/CONJ_TAC.doc
/usr/share/hol-light/Help/CONTR.doc
/usr/share/hol-light/Help/CONTRAPOS_CONV.doc
/usr/share/hol-light/Help/CONTR_TAC.doc
/usr/share/hol-light/Help/CONV_RULE.doc
/usr/share/hol-light/Help/CONV_TAC.doc
/usr/share/hol-light/Help/DEDUCT_ANTISYM_RULE.doc
/usr/share/hol-light/Help/DENUMERAL.doc
/usr/share/hol-light/Help/DEPTH_BINOP_CONV.doc
/usr/share/hol-light/Help/DEPTH_CONV.doc
/usr/share/hol-light/Help/DEPTH_SQCONV.doc
/usr/share/hol-light/Help/DESTRUCT_TAC.doc
/usr/share/hol-light/Help/DISCH.doc
/usr/share/hol-light/Help/DISCH_ALL.doc
/usr/share/hol-light/Help/DISCH_TAC.doc
/usr/share/hol-light/Help/DISCH_THEN.doc
/usr/share/hol-light/Help/DISJ1.doc
/usr/share/hol-light/Help/DISJ1_TAC.doc
/usr/share/hol-light/Help/DISJ2.doc
/usr/share/hol-light/Help/DISJ2_TAC.doc
/usr/share/hol-light/Help/DISJ_ACI_RULE.doc
/usr/share/hol-light/Help/DISJ_CANON_CONV.doc
/usr/share/hol-light/Help/DISJ_CASES.doc
/usr/share/hol-light/Help/DISJ_CASES_TAC.doc
/usr/share/hol-light/Help/DISJ_CASES_THEN.doc
/usr/share/hol-light/Help/DISJ_CASES_THEN2.doc
/usr/share/hol-light/Help/DNF_CONV.doc
/usr/share/hol-light/Help/EQF_ELIM.doc
/usr/share/hol-light/Help/EQF_INTRO.doc
/usr/share/hol-light/Help/EQT_ELIM.doc
/usr/share/hol-light/Help/EQT_INTRO.doc
/usr/share/hol-light/Help/EQ_IMP_RULE.doc
/usr/share/hol-light/Help/EQ_MP.doc
/usr/share/hol-light/Help/EQ_TAC.doc
/usr/share/hol-light/Help/ETA_CONV.doc
/usr/share/hol-light/Help/EVERY.doc
/usr/share/hol-light/Help/EVERY_ASSUM.doc
/usr/share/hol-light/Help/EVERY_CONV.doc
/usr/share/hol-light/Help/EVERY_TCL.doc
/usr/share/hol-light/Help/EXISTENCE.doc
/usr/share/hol-light/Help/EXISTS_EQUATION.doc
/usr/share/hol-light/Help/EXISTS_TAC.doc
/usr/share/hol-light/Help/EXISTS_UPPERCASE.doc
/usr/share/hol-light/Help/EXPAND_CASES_CONV.doc
/usr/share/hol-light/Help/EXPAND_TAC.doc
/usr/share/hol-light/Help/FAIL_TAC.doc
/usr/share/hol-light/Help/FIND_ASSUM.doc
/usr/share/hol-light/Help/FIRST.doc
/usr/share/hol-light/Help/FIRST_ASSUM.doc
/usr/share/hol-light/Help/FIRST_CONV.doc
/usr/share/hol-light/Help/FIRST_TCL.doc
/usr/share/hol-light/Help/FIRST_X_ASSUM.doc
/usr/share/hol-light/Help/FIX_TAC.doc
/usr/share/hol-light/Help/FORALL_UNWIND_CONV.doc
/usr/share/hol-light/Help/FREEZE_THEN.doc
/usr/share/hol-light/Help/F_F.doc
/usr/share/hol-light/Help/GABS_CONV.doc
/usr/share/hol-light/Help/GEN.doc
/usr/share/hol-light/Help/GENERAL_REWRITE_CONV.doc
/usr/share/hol-light/Help/GENL.doc
/usr/share/hol-light/Help/GEN_ALL.doc
/usr/share/hol-light/Help/GEN_ALPHA_CONV.doc
/usr/share/hol-light/Help/GEN_BETA_CONV.doc
/usr/share/hol-light/Help/GEN_MESON_TAC.doc
/usr/share/hol-light/Help/GEN_NNF_CONV.doc
/usr/share/hol-light/Help/GEN_PART_MATCH.doc
/usr/share/hol-light/Help/GEN_REAL_ARITH.doc
/usr/share/hol-light/Help/GEN_REWRITE_CONV.doc
/usr/share/hol-light/Help/GEN_REWRITE_RULE.doc
/usr/share/hol-light/Help/GEN_REWRITE_TAC.doc
/usr/share/hol-light/Help/GEN_SIMPLIFY_CONV.doc
/usr/share/hol-light/Help/GEN_TAC.doc
/usr/share/hol-light/Help/GSYM.doc
/usr/share/hol-light/Help/HAS_SIZE_CONV.doc
/usr/share/hol-light/Help/HIGHER_REWRITE_CONV.doc
/usr/share/hol-light/Help/HINT_EXISTS_TAC.doc
/usr/share/hol-light/Help/HYP_TAC.doc
/usr/share/hol-light/Help/HYP_UPPERCASE.doc
/usr/share/hol-light/Help/I.doc
/usr/share/hol-light/Help/IMP_ANTISYM_RULE.doc
/usr/share/hol-light/Help/IMP_RES_THEN.doc
/usr/share/hol-light/Help/IMP_REWRITE_TAC.doc
/usr/share/hol-light/Help/IMP_REWR_CONV.doc
/usr/share/hol-light/Help/IMP_TRANS.doc
/usr/share/hol-light/Help/INDUCT_TAC.doc
/usr/share/hol-light/Help/INSTANTIATE_ALL.doc
/usr/share/hol-light/Help/INSTANTIATE_UPPERCASE.doc
/usr/share/hol-light/Help/INST_TYPE.doc
/usr/share/hol-light/Help/INST_UPPERCASE.doc
/usr/share/hol-light/Help/INTEGER_RULE.doc
/usr/share/hol-light/Help/INTEGER_TAC.doc
/usr/share/hol-light/Help/INTRO_TAC.doc
/usr/share/hol-light/Help/INT_ABS_CONV.doc
/usr/share/hol-light/Help/INT_ADD_CONV.doc
/usr/share/hol-light/Help/INT_ARITH.doc
/usr/share/hol-light/Help/INT_ARITH_TAC.doc
/usr/share/hol-light/Help/INT_EQ_CONV.doc
/usr/share/hol-light/Help/INT_GE_CONV.doc
/usr/share/hol-light/Help/INT_GT_CONV.doc
/usr/share/hol-light/Help/INT_LE_CONV.doc
/usr/share/hol-light/Help/INT_LT_CONV.doc
/usr/share/hol-light/Help/INT_MAX_CONV.doc
/usr/share/hol-light/Help/INT_MIN_CONV.doc
/usr/share/hol-light/Help/INT_MUL_CONV.doc
/usr/share/hol-light/Help/INT_NEG_CONV.doc
/usr/share/hol-light/Help/INT_OF_REAL_THM.doc
/usr/share/hol-light/Help/INT_POLY_CONV.doc
/usr/share/hol-light/Help/INT_POW_CONV.doc
/usr/share/hol-light/Help/INT_REDUCE_CONV.doc
/usr/share/hol-light/Help/INT_RED_CONV.doc
/usr/share/hol-light/Help/INT_RING.doc
/usr/share/hol-light/Help/INT_SUB_CONV.doc
/usr/share/hol-light/Help/ISPEC.doc
/usr/share/hol-light/Help/ISPECL.doc
/usr/share/hol-light/Help/ITAUT.doc
/usr/share/hol-light/Help/ITAUT_TAC.doc
/usr/share/hol-light/Help/K.doc
/usr/share/hol-light/Help/LABEL_TAC.doc
/usr/share/hol-light/Help/LAMBDA_ELIM_CONV.doc
/usr/share/hol-light/Help/LAND_CONV.doc
/usr/share/hol-light/Help/LET_TAC.doc
/usr/share/hol-light/Help/LE_IMP.doc
/usr/share/hol-light/Help/LIST_CONV.doc
/usr/share/hol-light/Help/LIST_INDUCT_TAC.doc
/usr/share/hol-light/Help/MAP_EVERY.doc
/usr/share/hol-light/Help/MAP_FIRST.doc
/usr/share/hol-light/Help/MATCH_ACCEPT_TAC.doc
/usr/share/hol-light/Help/MATCH_CONV.doc
/usr/share/hol-light/Help/MATCH_MP.doc
/usr/share/hol-light/Help/MATCH_MP_TAC.doc
/usr/share/hol-light/Help/MESON.doc
/usr/share/hol-light/Help/MESON_TAC.doc
/usr/share/hol-light/Help/META_EXISTS_TAC.doc
/usr/share/hol-light/Help/META_SPEC_TAC.doc
/usr/share/hol-light/Help/METIS.doc
/usr/share/hol-light/Help/METIS_TAC.doc
/usr/share/hol-light/Help/MK_BINOP_UPPERCASE.doc
/usr/share/hol-light/Help/MK_COMB_TAC.doc
/usr/share/hol-light/Help/MK_COMB_UPPERCASE.doc
/usr/share/hol-light/Help/MK_CONJ_UPPERCASE.doc
/usr/share/hol-light/Help/MK_DISJ_UPPERCASE.doc
/usr/share/hol-light/Help/MK_EXISTS_UPPERCASE.doc
/usr/share/hol-light/Help/MK_FORALL_UPPERCASE.doc
/usr/share/hol-light/Help/MONO_TAC.doc
/usr/share/hol-light/Help/MP.doc
/usr/share/hol-light/Help/MP_CONV.doc
/usr/share/hol-light/Help/MP_TAC.doc
/usr/share/hol-light/Help/NNFC_CONV.doc
/usr/share/hol-light/Help/NNF_CONV.doc
/usr/share/hol-light/Help/NOT_ELIM.doc
/usr/share/hol-light/Help/NOT_INTRO.doc
/usr/share/hol-light/Help/NO_CONV.doc
/usr/share/hol-light/Help/NO_TAC.doc
/usr/share/hol-light/Help/NO_THEN.doc
/usr/share/hol-light/Help/NUMBER_RULE.doc
/usr/share/hol-light/Help/NUMBER_TAC.doc
/usr/share/hol-light/Help/NUMSEG_CONV.doc
/usr/share/hol-light/Help/NUM_ADD_CONV.doc
/usr/share/hol-light/Help/NUM_CANCEL_CONV.doc
/usr/share/hol-light/Help/NUM_DIV_CONV.doc
/usr/share/hol-light/Help/NUM_EQ_CONV.doc
/usr/share/hol-light/Help/NUM_EVEN_CONV.doc
/usr/share/hol-light/Help/NUM_EXP_CONV.doc
/usr/share/hol-light/Help/NUM_FACT_CONV.doc
/usr/share/hol-light/Help/NUM_GE_CONV.doc
/usr/share/hol-light/Help/NUM_GT_CONV.doc
/usr/share/hol-light/Help/NUM_LE_CONV.doc
/usr/share/hol-light/Help/NUM_LT_CONV.doc
/usr/share/hol-light/Help/NUM_MAX_CONV.doc
/usr/share/hol-light/Help/NUM_MIN_CONV.doc
/usr/share/hol-light/Help/NUM_MOD_CONV.doc
/usr/share/hol-light/Help/NUM_MULT_CONV.doc
/usr/share/hol-light/Help/NUM_NORMALIZE_CONV.doc
/usr/share/hol-light/Help/NUM_ODD_CONV.doc
/usr/share/hol-light/Help/NUM_PRE_CONV.doc
/usr/share/hol-light/Help/NUM_REDUCE_CONV.doc
/usr/share/hol-light/Help/NUM_REDUCE_TAC.doc
/usr/share/hol-light/Help/NUM_RED_CONV.doc
/usr/share/hol-light/Help/NUM_REL_CONV.doc
/usr/share/hol-light/Help/NUM_RING.doc
/usr/share/hol-light/Help/NUM_SIMPLIFY_CONV.doc
/usr/share/hol-light/Help/NUM_SUB_CONV.doc
/usr/share/hol-light/Help/NUM_SUC_CONV.doc
/usr/share/hol-light/Help/NUM_TO_INT_CONV.doc
/usr/share/hol-light/Help/ONCE_ASM_REWRITE_RULE.doc
/usr/share/hol-light/Help/ONCE_ASM_REWRITE_TAC.doc
/usr/share/hol-light/Help/ONCE_ASM_SIMP_TAC.doc
/usr/share/hol-light/Help/ONCE_DEPTH_CONV.doc
/usr/share/hol-light/Help/ONCE_DEPTH_SQCONV.doc
/usr/share/hol-light/Help/ONCE_REWRITE_CONV.doc
/usr/share/hol-light/Help/ONCE_REWRITE_RULE.doc
/usr/share/hol-light/Help/ONCE_REWRITE_TAC.doc
/usr/share/hol-light/Help/ONCE_SIMPLIFY_CONV.doc
/usr/share/hol-light/Help/ONCE_SIMP_CONV.doc
/usr/share/hol-light/Help/ONCE_SIMP_RULE.doc
/usr/share/hol-light/Help/ONCE_SIMP_TAC.doc
/usr/share/hol-light/Help/ORDERED_IMP_REWR_CONV.doc
/usr/share/hol-light/Help/ORDERED_REWR_CONV.doc
/usr/share/hol-light/Help/ORELSE.doc
/usr/share/hol-light/Help/ORELSEC.doc
/usr/share/hol-light/Help/ORELSE_TCL.doc
/usr/share/hol-light/Help/PART_MATCH.doc
/usr/share/hol-light/Help/PATH_CONV.doc
/usr/share/hol-light/Help/PAT_CONV.doc
/usr/share/hol-light/Help/PINST.doc
/usr/share/hol-light/Help/POP_ASSUM.doc
/usr/share/hol-light/Help/POP_ASSUM_LIST.doc
/usr/share/hol-light/Help/PRENEX_CONV.doc
/usr/share/hol-light/Help/PRESIMP_CONV.doc
/usr/share/hol-light/Help/PROP_ATOM_CONV.doc
/usr/share/hol-light/Help/PROVE_HYP.doc
/usr/share/hol-light/Help/PURE_ASM_REWRITE_RULE.doc
/usr/share/hol-light/Help/PURE_ASM_REWRITE_TAC.doc
/usr/share/hol-light/Help/PURE_ASM_SIMP_TAC.doc
/usr/share/hol-light/Help/PURE_ONCE_ASM_REWRITE_RULE.doc
/usr/share/hol-light/Help/PURE_ONCE_ASM_REWRITE_TAC.doc
/usr/share/hol-light/Help/PURE_ONCE_REWRITE_CONV.doc
/usr/share/hol-light/Help/PURE_ONCE_REWRITE_RULE.doc
/usr/share/hol-light/Help/PURE_ONCE_REWRITE_TAC.doc
/usr/share/hol-light/Help/PURE_REWRITE_CONV.doc
/usr/share/hol-light/Help/PURE_REWRITE_RULE.doc
/usr/share/hol-light/Help/PURE_REWRITE_TAC.doc
/usr/share/hol-light/Help/PURE_SIMP_CONV.doc
/usr/share/hol-light/Help/PURE_SIMP_RULE.doc
/usr/share/hol-light/Help/PURE_SIMP_TAC.doc
/usr/share/hol-light/Help/RAND_CONV.doc
/usr/share/hol-light/Help/RATOR_CONV.doc
/usr/share/hol-light/Help/REAL_ARITH.doc
/usr/share/hol-light/Help/REAL_ARITH_TAC.doc
/usr/share/hol-light/Help/REAL_FIELD.doc
/usr/share/hol-light/Help/REAL_IDEAL_CONV.doc
/usr/share/hol-light/Help/REAL_INT_ABS_CONV.doc
/usr/share/hol-light/Help/REAL_INT_ADD_CONV.doc
/usr/share/hol-light/Help/REAL_INT_EQ_CONV.doc
/usr/share/hol-light/Help/REAL_INT_GE_CONV.doc
/usr/share/hol-light/Help/REAL_INT_GT_CONV.doc
/usr/share/hol-light/Help/REAL_INT_LE_CONV.doc
/usr/share/hol-light/Help/REAL_INT_LT_CONV.doc
/usr/share/hol-light/Help/REAL_INT_MUL_CONV.doc
/usr/share/hol-light/Help/REAL_INT_NEG_CONV.doc
/usr/share/hol-light/Help/REAL_INT_POW_CONV.doc
/usr/share/hol-light/Help/REAL_INT_RAT_CONV.doc
/usr/share/hol-light/Help/REAL_INT_REDUCE_CONV.doc
/usr/share/hol-light/Help/REAL_INT_RED_CONV.doc
/usr/share/hol-light/Help/REAL_INT_SUB_CONV.doc
/usr/share/hol-light/Help/REAL_LET_IMP.doc
/usr/share/hol-light/Help/REAL_LE_IMP.doc
/usr/share/hol-light/Help/REAL_LINEAR_PROVER.doc
/usr/share/hol-light/Help/REAL_POLY_ADD_CONV.doc
/usr/share/hol-light/Help/REAL_POLY_CONV.doc
/usr/share/hol-light/Help/REAL_POLY_MUL_CONV.doc
/usr/share/hol-light/Help/REAL_POLY_NEG_CONV.doc
/usr/share/hol-light/Help/REAL_POLY_POW_CONV.doc
/usr/share/hol-light/Help/REAL_POLY_SUB_CONV.doc
/usr/share/hol-light/Help/REAL_RAT_ABS_CONV.doc
/usr/share/hol-light/Help/REAL_RAT_ADD_CONV.doc
/usr/share/hol-light/Help/REAL_RAT_DIV_CONV.doc
/usr/share/hol-light/Help/REAL_RAT_EQ_CONV.doc
/usr/share/hol-light/Help/REAL_RAT_GE_CONV.doc
/usr/share/hol-light/Help/REAL_RAT_GT_CONV.doc
/usr/share/hol-light/Help/REAL_RAT_INV_CONV.doc
/usr/share/hol-light/Help/REAL_RAT_LE_CONV.doc
/usr/share/hol-light/Help/REAL_RAT_LT_CONV.doc
/usr/share/hol-light/Help/REAL_RAT_MAX_CONV.doc
/usr/share/hol-light/Help/REAL_RAT_MIN_CONV.doc
/usr/share/hol-light/Help/REAL_RAT_MUL_CONV.doc
/usr/share/hol-light/Help/REAL_RAT_NEG_CONV.doc
/usr/share/hol-light/Help/REAL_RAT_POW_CONV.doc
/usr/share/hol-light/Help/REAL_RAT_REDUCE_CONV.doc
/usr/share/hol-light/Help/REAL_RAT_RED_CONV.doc
/usr/share/hol-light/Help/REAL_RAT_SUB_CONV.doc
/usr/share/hol-light/Help/REAL_RING.doc
/usr/share/hol-light/Help/RECALL_ACCEPT_TAC.doc
/usr/share/hol-light/Help/REDEPTH_CONV.doc
/usr/share/hol-light/Help/REDEPTH_SQCONV.doc
/usr/share/hol-light/Help/REFL.doc
/usr/share/hol-light/Help/REFL_TAC.doc
/usr/share/hol-light/Help/REFUTE_THEN.doc
/usr/share/hol-light/Help/REMOVE_THEN.doc
/usr/share/hol-light/Help/REPEATC.doc
/usr/share/hol-light/Help/REPEAT_GTCL.doc
/usr/share/hol-light/Help/REPEAT_TCL.doc
/usr/share/hol-light/Help/REPEAT_UPPERCASE.doc
/usr/share/hol-light/Help/REPLICATE_TAC.doc
/usr/share/hol-light/Help/REWRITES_CONV.doc
/usr/share/hol-light/Help/REWRITE_CONV.doc
/usr/share/hol-light/Help/REWRITE_RULE.doc
/usr/share/hol-light/Help/REWRITE_TAC.doc
/usr/share/hol-light/Help/REWR_CONV.doc
/usr/share/hol-light/Help/RIGHT_BETAS.doc
/usr/share/hol-light/Help/RING.doc
/usr/share/hol-light/Help/RING_AND_IDEAL_CONV.doc
/usr/share/hol-light/Help/RULE_ASSUM_TAC.doc
/usr/share/hol-light/Help/SELECT_CONV.doc
/usr/share/hol-light/Help/SELECT_ELIM_TAC.doc
/usr/share/hol-light/Help/SELECT_RULE.doc
/usr/share/hol-light/Help/SEMIRING_NORMALIZERS_CONV.doc
/usr/share/hol-light/Help/SEQ_IMP_REWRITE_TAC.doc
/usr/share/hol-light/Help/SET_RULE.doc
/usr/share/hol-light/Help/SET_TAC.doc
/usr/share/hol-light/Help/SIMPLE_CHOOSE.doc
/usr/share/hol-light/Help/SIMPLE_DISJ_CASES.doc
/usr/share/hol-light/Help/SIMPLE_EXISTS.doc
/usr/share/hol-light/Help/SIMPLIFY_CONV.doc
/usr/share/hol-light/Help/SIMP_CONV.doc
/usr/share/hol-light/Help/SIMP_RULE.doc
/usr/share/hol-light/Help/SIMP_TAC.doc
/usr/share/hol-light/Help/SKOLEM_CONV.doc
/usr/share/hol-light/Help/SPEC.doc
/usr/share/hol-light/Help/SPECL.doc
/usr/share/hol-light/Help/SPEC_ALL.doc
/usr/share/hol-light/Help/SPEC_TAC.doc
/usr/share/hol-light/Help/SPEC_VAR.doc
/usr/share/hol-light/Help/STRING_EQ_CONV.doc
/usr/share/hol-light/Help/STRIP_ASSUME_TAC.doc
/usr/share/hol-light/Help/STRIP_GOAL_THEN.doc
/usr/share/hol-light/Help/STRIP_TAC.doc
/usr/share/hol-light/Help/STRIP_THM_THEN.doc
/usr/share/hol-light/Help/STRUCT_CASES_TAC.doc
/usr/share/hol-light/Help/STRUCT_CASES_THEN.doc
/usr/share/hol-light/Help/SUBGOAL_TAC.doc
/usr/share/hol-light/Help/SUBGOAL_THEN.doc
/usr/share/hol-light/Help/SUBS.doc
/usr/share/hol-light/Help/SUBST1_TAC.doc
/usr/share/hol-light/Help/SUBST_ALL_TAC.doc
/usr/share/hol-light/Help/SUBST_VAR_TAC.doc
/usr/share/hol-light/Help/SUBS_CONV.doc
/usr/share/hol-light/Help/SUB_CONV.doc
/usr/share/hol-light/Help/SYM.doc
/usr/share/hol-light/Help/SYM_CONV.doc
/usr/share/hol-light/Help/TAC_PROOF.doc
/usr/share/hol-light/Help/TARGET_REWRITE_TAC.doc
/usr/share/hol-light/Help/TAUT.doc
/usr/share/hol-light/Help/THEN.doc
/usr/share/hol-light/Help/THENC.doc
/usr/share/hol-light/Help/THENL.doc
/usr/share/hol-light/Help/THEN_TCL.doc
/usr/share/hol-light/Help/TOP_DEPTH_CONV.doc
/usr/share/hol-light/Help/TOP_DEPTH_SQCONV.doc
/usr/share/hol-light/Help/TOP_SWEEP_CONV.doc
/usr/share/hol-light/Help/TOP_SWEEP_SQCONV.doc
/usr/share/hol-light/Help/TRANS.doc
/usr/share/hol-light/Help/TRANS_TAC.doc
/usr/share/hol-light/Help/TRY.doc
/usr/share/hol-light/Help/TRY_CONV.doc
/usr/share/hol-light/Help/UNDISCH.doc
/usr/share/hol-light/Help/UNDISCH_ALL.doc
/usr/share/hol-light/Help/UNDISCH_TAC.doc
/usr/share/hol-light/Help/UNDISCH_THEN.doc
/usr/share/hol-light/Help/UNIFY_ACCEPT_TAC.doc
/usr/share/hol-light/Help/UNWIND_CONV.doc
/usr/share/hol-light/Help/USE_THEN.doc
/usr/share/hol-light/Help/VALID.doc
/usr/share/hol-light/Help/W.doc
/usr/share/hol-light/Help/WEAK_CNF_CONV.doc
/usr/share/hol-light/Help/WEAK_DNF_CONV.doc
/usr/share/hol-light/Help/WF_INDUCT_TAC.doc
/usr/share/hol-light/Help/X_CHOOSE_TAC.doc
/usr/share/hol-light/Help/X_CHOOSE_THEN.doc
/usr/share/hol-light/Help/X_GEN_TAC.doc
/usr/share/hol-light/Help/X_META_EXISTS_TAC.doc
/usr/share/hol-light/Help/a.doc
/usr/share/hol-light/Help/aconv.doc
/usr/share/hol-light/Help/allpairs.doc
/usr/share/hol-light/Help/alpha.doc
/usr/share/hol-light/Help/alphaorder.doc
/usr/share/hol-light/Help/apply.doc
/usr/share/hol-light/Help/apply_prover.doc
/usr/share/hol-light/Help/applyd.doc
/usr/share/hol-light/Help/assoc.doc
/usr/share/hol-light/Help/assocd.doc
/usr/share/hol-light/Help/atleast.doc
/usr/share/hol-light/Help/aty.doc
/usr/share/hol-light/Help/augment.doc
/usr/share/hol-light/Help/axioms.doc
/usr/share/hol-light/Help/b.doc
/usr/share/hol-light/Help/basic_congs.doc
/usr/share/hol-light/Help/basic_convs.doc
/usr/share/hol-light/Help/basic_net.doc
/usr/share/hol-light/Help/basic_prover.doc
/usr/share/hol-light/Help/basic_rectype_net.doc
/usr/share/hol-light/Help/basic_rewrites.doc
/usr/share/hol-light/Help/basic_ss.doc
/usr/share/hol-light/Help/binders.doc
/usr/share/hol-light/Help/binops.doc
/usr/share/hol-light/Help/bndvar.doc
/usr/share/hol-light/Help/body.doc
/usr/share/hol-light/Help/bool_ty.doc
/usr/share/hol-light/Help/bty.doc
/usr/share/hol-light/Help/butlast.doc
/usr/share/hol-light/Help/by.doc
/usr/share/hol-light/Help/can.doc
/usr/share/hol-light/Help/cases.doc
/usr/share/hol-light/Help/check.doc
/usr/share/hol-light/Help/checkpoint.doc
/usr/share/hol-light/Help/choose.doc
/usr/share/hol-light/Help/chop_list.doc
/usr/share/hol-light/Help/combine.doc
/usr/share/hol-light/Help/comment_token.doc
/usr/share/hol-light/Help/compose_insts.doc
/usr/share/hol-light/Help/concl.doc
/usr/share/hol-light/Help/conjuncts.doc
/usr/share/hol-light/Help/constants.doc
/usr/share/hol-light/Help/current_goalstack.doc
/usr/share/hol-light/Help/curry.doc
/usr/share/hol-light/Help/decreasing.doc
/usr/share/hol-light/Help/deep_alpha.doc
/usr/share/hol-light/Help/define.doc
/usr/share/hol-light/Help/define_finite_type.doc
/usr/share/hol-light/Help/define_quotient_type.doc
/usr/share/hol-light/Help/define_type.doc
/usr/share/hol-light/Help/define_type_raw.doc
/usr/share/hol-light/Help/defined.doc
/usr/share/hol-light/Help/definitions.doc
/usr/share/hol-light/Help/delete_parser.doc
/usr/share/hol-light/Help/delete_user_printer.doc
/usr/share/hol-light/Help/denominator.doc
/usr/share/hol-light/Help/derive_nonschematic_inductive_relations.doc
/usr/share/hol-light/Help/derive_strong_induction.doc
/usr/share/hol-light/Help/dest_abs.doc
/usr/share/hol-light/Help/dest_binary.doc
/usr/share/hol-light/Help/dest_binder.doc
/usr/share/hol-light/Help/dest_binop.doc
/usr/share/hol-light/Help/dest_char.doc
/usr/share/hol-light/Help/dest_comb.doc
/usr/share/hol-light/Help/dest_cond.doc
/usr/share/hol-light/Help/dest_conj.doc
/usr/share/hol-light/Help/dest_cons.doc
/usr/share/hol-light/Help/dest_const.doc
/usr/share/hol-light/Help/dest_disj.doc
/usr/share/hol-light/Help/dest_eq.doc
/usr/share/hol-light/Help/dest_exists.doc
/usr/share/hol-light/Help/dest_forall.doc
/usr/share/hol-light/Help/dest_fun_ty.doc
/usr/share/hol-light/Help/dest_gabs.doc
/usr/share/hol-light/Help/dest_iff.doc
/usr/share/hol-light/Help/dest_imp.doc
/usr/share/hol-light/Help/dest_intconst.doc
/usr/share/hol-light/Help/dest_let.doc
/usr/share/hol-light/Help/dest_list.doc
/usr/share/hol-light/Help/dest_neg.doc
/usr/share/hol-light/Help/dest_numeral.doc
/usr/share/hol-light/Help/dest_pair.doc
/usr/share/hol-light/Help/dest_realintconst.doc
/usr/share/hol-light/Help/dest_select.doc
/usr/share/hol-light/Help/dest_setenum.doc
/usr/share/hol-light/Help/dest_small_numeral.doc
/usr/share/hol-light/Help/dest_string.doc
/usr/share/hol-light/Help/dest_thm.doc
/usr/share/hol-light/Help/dest_type.doc
/usr/share/hol-light/Help/dest_uexists.doc
/usr/share/hol-light/Help/dest_var.doc
/usr/share/hol-light/Help/dest_vartype.doc
/usr/share/hol-light/Help/disjuncts.doc
/usr/share/hol-light/Help/distinctness.doc
/usr/share/hol-light/Help/distinctness_store.doc
/usr/share/hol-light/Help/do_list.doc
/usr/share/hol-light/Help/dom.doc
/usr/share/hol-light/Help/dpty.doc
/usr/share/hol-light/Help/e.doc
/usr/share/hol-light/Help/el.doc
/usr/share/hol-light/Help/elistof.doc
/usr/share/hol-light/Help/empty_net.doc
/usr/share/hol-light/Help/empty_ss.doc
/usr/share/hol-light/Help/end_itlist.doc
/usr/share/hol-light/Help/enter.doc
/usr/share/hol-light/Help/equals_goal.doc
/usr/share/hol-light/Help/equals_thm.doc
/usr/share/hol-light/Help/exactly.doc
/usr/share/hol-light/Help/exists.doc
/usr/share/hol-light/Help/explode.doc
/usr/share/hol-light/Help/extend_basic_congs.doc
/usr/share/hol-light/Help/extend_basic_convs.doc
/usr/share/hol-light/Help/extend_basic_rewrites.doc
/usr/share/hol-light/Help/extend_rectype_net.doc
/usr/share/hol-light/Help/f_f_.doc
/usr/share/hol-light/Help/fail.doc
/usr/share/hol-light/Help/file_of_string.doc
/usr/share/hol-light/Help/file_on_path.doc
/usr/share/hol-light/Help/filter.doc
/usr/share/hol-light/Help/find.doc
/usr/share/hol-light/Help/find_path.doc
/usr/share/hol-light/Help/find_term.doc
/usr/share/hol-light/Help/find_terms.doc
/usr/share/hol-light/Help/finished.doc
/usr/share/hol-light/Help/fix.doc
/usr/share/hol-light/Help/flat.doc
/usr/share/hol-light/Help/flush_goalstack.doc
/usr/share/hol-light/Help/foldl.doc
/usr/share/hol-light/Help/foldr.doc
/usr/share/hol-light/Help/follow_path.doc
/usr/share/hol-light/Help/forall.doc
/usr/share/hol-light/Help/forall2.doc
/usr/share/hol-light/Help/free_in.doc
/usr/share/hol-light/Help/frees.doc
/usr/share/hol-light/Help/freesin.doc
/usr/share/hol-light/Help/freesl.doc
/usr/share/hol-light/Help/funpow.doc
/usr/share/hol-light/Help/g.doc
/usr/share/hol-light/Help/gcd.doc
/usr/share/hol-light/Help/gcd_num.doc
/usr/share/hol-light/Help/genvar.doc
/usr/share/hol-light/Help/get_const_type.doc
/usr/share/hol-light/Help/get_infix_status.doc
/usr/share/hol-light/Help/get_type_arity.doc
/usr/share/hol-light/Help/graph.doc
/usr/share/hol-light/Help/hd.doc
/usr/share/hol-light/Help/help.doc
/usr/share/hol-light/Help/help_path.doc
/usr/share/hol-light/Help/hide_constant.doc
/usr/share/hol-light/Help/hol_dir.doc
/usr/share/hol-light/Help/hol_expand_directory.doc
/usr/share/hol-light/Help/hol_version.doc
/usr/share/hol-light/Help/hyp.doc
/usr/share/hol-light/Help/ideal_cofactors.doc
/usr/share/hol-light/Help/ignore_constant_varstruct.doc
/usr/share/hol-light/Help/implode.doc
/usr/share/hol-light/Help/increasing.doc
/usr/share/hol-light/Help/index.doc
/usr/share/hol-light/Help/inductive_type_store.doc
/usr/share/hol-light/Help/infixes.doc
/usr/share/hol-light/Help/injectivity.doc
/usr/share/hol-light/Help/injectivity_store.doc
/usr/share/hol-light/Help/insert.doc
/usr/share/hol-light/Help/insert_prime.doc
/usr/share/hol-light/Help/inst.doc
/usr/share/hol-light/Help/inst_goal.doc
/usr/share/hol-light/Help/install_parser.doc
/usr/share/hol-light/Help/install_user_printer.doc
/usr/share/hol-light/Help/installed_parsers.doc
/usr/share/hol-light/Help/instantiate.doc
/usr/share/hol-light/Help/instantiate_casewise_recursion.doc
/usr/share/hol-light/Help/int_ideal_cofactors.doc
/usr/share/hol-light/Help/intersect.doc
/usr/share/hol-light/Help/is_abs.doc
/usr/share/hol-light/Help/is_binary.doc
/usr/share/hol-light/Help/is_binder.doc
/usr/share/hol-light/Help/is_binop.doc
/usr/share/hol-light/Help/is_comb.doc
/usr/share/hol-light/Help/is_cond.doc
/usr/share/hol-light/Help/is_conj.doc
/usr/share/hol-light/Help/is_cons.doc
/usr/share/hol-light/Help/is_const.doc
/usr/share/hol-light/Help/is_disj.doc
/usr/share/hol-light/Help/is_eq.doc
/usr/share/hol-light/Help/is_exists.doc
/usr/share/hol-light/Help/is_forall.doc
/usr/share/hol-light/Help/is_gabs.doc
/usr/share/hol-light/Help/is_hidden.doc
/usr/share/hol-light/Help/is_iff.doc
/usr/share/hol-light/Help/is_imp.doc
/usr/share/hol-light/Help/is_intconst.doc
/usr/share/hol-light/Help/is_let.doc
/usr/share/hol-light/Help/is_list.doc
/usr/share/hol-light/Help/is_neg.doc
/usr/share/hol-light/Help/is_numeral.doc
/usr/share/hol-light/Help/is_pair.doc
/usr/share/hol-light/Help/is_prefix.doc
/usr/share/hol-light/Help/is_ratconst.doc
/usr/share/hol-light/Help/is_realintconst.doc
/usr/share/hol-light/Help/is_reserved_word.doc
/usr/share/hol-light/Help/is_select.doc
/usr/share/hol-light/Help/is_setenum.doc
/usr/share/hol-light/Help/is_type.doc
/usr/share/hol-light/Help/is_uexists.doc
/usr/share/hol-light/Help/is_undefined.doc
/usr/share/hol-light/Help/is_var.doc
/usr/share/hol-light/Help/is_vartype.doc
/usr/share/hol-light/Help/isalnum.doc
/usr/share/hol-light/Help/isalpha.doc
/usr/share/hol-light/Help/isbra.doc
/usr/share/hol-light/Help/isnum.doc
/usr/share/hol-light/Help/issep.doc
/usr/share/hol-light/Help/isspace.doc
/usr/share/hol-light/Help/issymb.doc
/usr/share/hol-light/Help/it.doc
/usr/share/hol-light/Help/itlist.doc
/usr/share/hol-light/Help/itlist2.doc
/usr/share/hol-light/Help/last.doc
/usr/share/hol-light/Help/lcm_num.doc
/usr/share/hol-light/Help/leftbin.doc
/usr/share/hol-light/Help/length.doc
/usr/share/hol-light/Help/let_CONV.doc
/usr/share/hol-light/Help/lex.doc
/usr/share/hol-light/Help/lhand.doc
/usr/share/hol-light/Help/lhs.doc
/usr/share/hol-light/Help/lift_function.doc
/usr/share/hol-light/Help/lift_theorem.doc
/usr/share/hol-light/Help/list_mk_abs.doc
/usr/share/hol-light/Help/list_mk_binop.doc
/usr/share/hol-light/Help/list_mk_comb.doc
/usr/share/hol-light/Help/list_mk_conj.doc
/usr/share/hol-light/Help/list_mk_disj.doc
/usr/share/hol-light/Help/list_mk_exists.doc
/usr/share/hol-light/Help/list_mk_forall.doc
/usr/share/hol-light/Help/list_mk_gabs.doc
/usr/share/hol-light/Help/list_mk_icomb.doc
/usr/share/hol-light/Help/listof.doc
/usr/share/hol-light/Help/load_on_path.doc
/usr/share/hol-light/Help/load_path.doc
/usr/share/hol-light/Help/loaded_files.doc
/usr/share/hol-light/Help/loads.doc
/usr/share/hol-light/Help/loadt.doc
/usr/share/hol-light/Help/lookup.doc
/usr/share/hol-light/Help/make_args.doc
/usr/share/hol-light/Help/make_overloadable.doc
/usr/share/hol-light/Help/many.doc
/usr/share/hol-light/Help/map.doc
/usr/share/hol-light/Help/map2.doc
/usr/share/hol-light/Help/mapf.doc
/usr/share/hol-light/Help/mapfilter.doc
/usr/share/hol-light/Help/mem.doc
/usr/share/hol-light/Help/mem_prime.doc
/usr/share/hol-light/Help/merge.doc
/usr/share/hol-light/Help/merge_nets.doc
/usr/share/hol-light/Help/mergesort.doc
/usr/share/hol-light/Help/meson_brand.doc
/usr/share/hol-light/Help/meson_chatty.doc
/usr/share/hol-light/Help/meson_dcutin.doc
/usr/share/hol-light/Help/meson_depth.doc
/usr/share/hol-light/Help/meson_prefine.doc
/usr/share/hol-light/Help/meson_skew.doc
/usr/share/hol-light/Help/meson_split_limit.doc
/usr/share/hol-light/Help/mk_abs.doc
/usr/share/hol-light/Help/mk_binary.doc
/usr/share/hol-light/Help/mk_binder.doc
/usr/share/hol-light/Help/mk_binop.doc
/usr/share/hol-light/Help/mk_char.doc
/usr/share/hol-light/Help/mk_comb.doc
/usr/share/hol-light/Help/mk_cond.doc
/usr/share/hol-light/Help/mk_conj.doc
/usr/share/hol-light/Help/mk_cons.doc
/usr/share/hol-light/Help/mk_const.doc
/usr/share/hol-light/Help/mk_disj.doc
/usr/share/hol-light/Help/mk_eq.doc
/usr/share/hol-light/Help/mk_exists.doc
/usr/share/hol-light/Help/mk_flist.doc
/usr/share/hol-light/Help/mk_forall.doc
/usr/share/hol-light/Help/mk_fset.doc
/usr/share/hol-light/Help/mk_fthm.doc
/usr/share/hol-light/Help/mk_fun_ty.doc
/usr/share/hol-light/Help/mk_gabs.doc
/usr/share/hol-light/Help/mk_goalstate.doc
/usr/share/hol-light/Help/mk_icomb.doc
/usr/share/hol-light/Help/mk_iff.doc
/usr/share/hol-light/Help/mk_imp.doc
/usr/share/hol-light/Help/mk_intconst.doc
/usr/share/hol-light/Help/mk_let.doc
/usr/share/hol-light/Help/mk_list.doc
/usr/share/hol-light/Help/mk_mconst.doc
/usr/share/hol-light/Help/mk_neg.doc
/usr/share/hol-light/Help/mk_numeral.doc
/usr/share/hol-light/Help/mk_pair.doc
/usr/share/hol-light/Help/mk_primed_var.doc
/usr/share/hol-light/Help/mk_prover.doc
/usr/share/hol-light/Help/mk_realintconst.doc
/usr/share/hol-light/Help/mk_rewrites.doc
/usr/share/hol-light/Help/mk_select.doc
/usr/share/hol-light/Help/mk_setenum.doc
/usr/share/hol-light/Help/mk_small_numeral.doc
/usr/share/hol-light/Help/mk_string.doc
/usr/share/hol-light/Help/mk_thm.doc
/usr/share/hol-light/Help/mk_type.doc
/usr/share/hol-light/Help/mk_uexists.doc
/usr/share/hol-light/Help/mk_var.doc
/usr/share/hol-light/Help/mk_vartype.doc
/usr/share/hol-light/Help/monotonicity_theorems.doc
/usr/share/hol-light/Help/name.doc
/usr/share/hol-light/Help/name_of.doc
/usr/share/hol-light/Help/needs.doc
/usr/share/hol-light/Help/net_of_cong.doc
/usr/share/hol-light/Help/net_of_conv.doc
/usr/share/hol-light/Help/net_of_thm.doc
/usr/share/hol-light/Help/new_axiom.doc
/usr/share/hol-light/Help/new_basic_definition.doc
/usr/share/hol-light/Help/new_basic_type_definition.doc
/usr/share/hol-light/Help/new_constant.doc
/usr/share/hol-light/Help/new_definition.doc
/usr/share/hol-light/Help/new_inductive_definition.doc
/usr/share/hol-light/Help/new_inductive_set.doc
/usr/share/hol-light/Help/new_recursive_definition.doc
/usr/share/hol-light/Help/new_specification.doc
/usr/share/hol-light/Help/new_type.doc
/usr/share/hol-light/Help/new_type_abbrev.doc
/usr/share/hol-light/Help/new_type_definition.doc
/usr/share/hol-light/Help/nothing.doc
/usr/share/hol-light/Help/nsplit.doc
/usr/share/hol-light/Help/null_inst.doc
/usr/share/hol-light/Help/null_meta.doc
/usr/share/hol-light/Help/num_0.doc
/usr/share/hol-light/Help/num_1.doc
/usr/share/hol-light/Help/num_10.doc
/usr/share/hol-light/Help/num_2.doc
/usr/share/hol-light/Help/num_CONV.doc
/usr/share/hol-light/Help/num_of_string.doc
/usr/share/hol-light/Help/numdom.doc
/usr/share/hol-light/Help/numerator.doc
/usr/share/hol-light/Help/o.doc
/usr/share/hol-light/Help/occurs_in.doc
/usr/share/hol-light/Help/omit.doc
/usr/share/hol-light/Help/orelse_.doc
/usr/share/hol-light/Help/orelse_tcl_.doc
/usr/share/hol-light/Help/orelsec_.doc
/usr/share/hol-light/Help/overload_interface.doc
/usr/share/hol-light/Help/override_interface.doc
/usr/share/hol-light/Help/p.doc
/usr/share/hol-light/Help/parse_as_binder.doc
/usr/share/hol-light/Help/parse_as_infix.doc
/usr/share/hol-light/Help/parse_as_prefix.doc
/usr/share/hol-light/Help/parse_inductive_type_specification.doc
/usr/share/hol-light/Help/parse_preterm.doc
/usr/share/hol-light/Help/parse_pretype.doc
/usr/share/hol-light/Help/parse_term.doc
/usr/share/hol-light/Help/parse_type.doc
/usr/share/hol-light/Help/parses_as_binder.doc
/usr/share/hol-light/Help/partition.doc
/usr/share/hol-light/Help/possibly.doc
/usr/share/hol-light/Help/pow10.doc
/usr/share/hol-light/Help/pow2.doc
/usr/share/hol-light/Help/pp_print_qterm.doc
/usr/share/hol-light/Help/pp_print_qtype.doc
/usr/share/hol-light/Help/pp_print_term.doc
/usr/share/hol-light/Help/pp_print_thm.doc
/usr/share/hol-light/Help/pp_print_type.doc
/usr/share/hol-light/Help/prebroken_binops.doc
/usr/share/hol-light/Help/prefixes.doc
/usr/share/hol-light/Help/preterm_of_term.doc
/usr/share/hol-light/Help/pretype_of_type.doc
/usr/share/hol-light/Help/print_all_thm.doc
/usr/share/hol-light/Help/print_fpf.doc
/usr/share/hol-light/Help/print_goal.doc
/usr/share/hol-light/Help/print_goalstack.doc
/usr/share/hol-light/Help/print_num.doc
/usr/share/hol-light/Help/print_qterm.doc
/usr/share/hol-light/Help/print_qtype.doc
/usr/share/hol-light/Help/print_term.doc
/usr/share/hol-light/Help/print_thm.doc
/usr/share/hol-light/Help/print_to_string.doc
/usr/share/hol-light/Help/print_type.doc
/usr/share/hol-light/Help/print_unambiguous_comprehensions.doc
/usr/share/hol-light/Help/prioritize_int.doc
/usr/share/hol-light/Help/prioritize_num.doc
/usr/share/hol-light/Help/prioritize_overload.doc
/usr/share/hol-light/Help/prioritize_real.doc
/usr/share/hol-light/Help/prove.doc
/usr/share/hol-light/Help/prove_cases_thm.doc
/usr/share/hol-light/Help/prove_constructors_distinct.doc
/usr/share/hol-light/Help/prove_constructors_injective.doc
/usr/share/hol-light/Help/prove_general_recursive_function_exists.doc
/usr/share/hol-light/Help/prove_inductive_relations_exist.doc
/usr/share/hol-light/Help/prove_monotonicity_hyps.doc
/usr/share/hol-light/Help/prove_recursive_functions_exist.doc
/usr/share/hol-light/Help/pure_prove_recursive_function_exists.doc
/usr/share/hol-light/Help/qmap.doc
/usr/share/hol-light/Help/quotexpander.doc
/usr/share/hol-light/Help/r.doc
/usr/share/hol-light/Help/ran.doc
/usr/share/hol-light/Help/rand.doc
/usr/share/hol-light/Help/rat_of_term.doc
/usr/share/hol-light/Help/rator.doc
/usr/share/hol-light/Help/real_ideal_cofactors.doc
/usr/share/hol-light/Help/reduce_interface.doc
/usr/share/hol-light/Help/refine.doc
/usr/share/hol-light/Help/remark.doc
/usr/share/hol-light/Help/remove.doc
/usr/share/hol-light/Help/remove_interface.doc
/usr/share/hol-light/Help/remove_type_abbrev.doc
/usr/share/hol-light/Help/repeat.doc
/usr/share/hol-light/Help/replicate.doc
/usr/share/hol-light/Help/report.doc
/usr/share/hol-light/Help/report_timing.doc
/usr/share/hol-light/Help/reserve_words.doc
/usr/share/hol-light/Help/reserved_words.doc
/usr/share/hol-light/Help/retypecheck.doc
/usr/share/hol-light/Help/rev.doc
/usr/share/hol-light/Help/rev_assoc.doc
/usr/share/hol-light/Help/rev_assocd.doc
/usr/share/hol-light/Help/rev_itlist.doc
/usr/share/hol-light/Help/rev_itlist2.doc
/usr/share/hol-light/Help/rev_splitlist.doc
/usr/share/hol-light/Help/reverse_interface_mapping.doc
/usr/share/hol-light/Help/rhs.doc
/usr/share/hol-light/Help/rightbin.doc
/usr/share/hol-light/Help/rotate.doc
/usr/share/hol-light/Help/search.doc
/usr/share/hol-light/Help/self_destruct.doc
/usr/share/hol-light/Help/set_basic_congs.doc
/usr/share/hol-light/Help/set_basic_convs.doc
/usr/share/hol-light/Help/set_basic_rewrites.doc
/usr/share/hol-light/Help/set_eq.doc
/usr/share/hol-light/Help/set_goal.doc
/usr/share/hol-light/Help/setify.doc
/usr/share/hol-light/Help/shareout.doc
/usr/share/hol-light/Help/some.doc
/usr/share/hol-light/Help/sort.doc
/usr/share/hol-light/Help/splitlist.doc
/usr/share/hol-light/Help/ss_of_congs.doc
/usr/share/hol-light/Help/ss_of_conv.doc
/usr/share/hol-light/Help/ss_of_maker.doc
/usr/share/hol-light/Help/ss_of_prover.doc
/usr/share/hol-light/Help/ss_of_provers.doc
/usr/share/hol-light/Help/ss_of_thms.doc
/usr/share/hol-light/Help/startup_banner.doc
/usr/share/hol-light/Help/string_of_file.doc
/usr/share/hol-light/Help/string_of_term.doc
/usr/share/hol-light/Help/string_of_thm.doc
/usr/share/hol-light/Help/string_of_type.doc
/usr/share/hol-light/Help/strings_of_file.doc
/usr/share/hol-light/Help/strip_abs.doc
/usr/share/hol-light/Help/strip_comb.doc
/usr/share/hol-light/Help/strip_exists.doc
/usr/share/hol-light/Help/strip_forall.doc
/usr/share/hol-light/Help/strip_gabs.doc
/usr/share/hol-light/Help/strip_ncomb.doc
/usr/share/hol-light/Help/striplist.doc
/usr/share/hol-light/Help/subset.doc
/usr/share/hol-light/Help/subst.doc
/usr/share/hol-light/Help/subtract.doc
/usr/share/hol-light/Help/subtract_prime.doc
/usr/share/hol-light/Help/temp_path.doc
/usr/share/hol-light/Help/term_match.doc
/usr/share/hol-light/Help/term_of_preterm.doc
/usr/share/hol-light/Help/term_of_rat.doc
/usr/share/hol-light/Help/term_order.doc
/usr/share/hol-light/Help/term_unify.doc
/usr/share/hol-light/Help/term_union.doc
/usr/share/hol-light/Help/the_definitions.doc
/usr/share/hol-light/Help/the_implicit_types.doc
/usr/share/hol-light/Help/the_inductive_definitions.doc
/usr/share/hol-light/Help/the_inductive_types.doc
/usr/share/hol-light/Help/the_interface.doc
/usr/share/hol-light/Help/the_overload_skeletons.doc
/usr/share/hol-light/Help/the_specifications.doc
/usr/share/hol-light/Help/the_type_definitions.doc
/usr/share/hol-light/Help/then_.doc
/usr/share/hol-light/Help/then_tcl_.doc
/usr/share/hol-light/Help/thenc_.doc
/usr/share/hol-light/Help/thenl_.doc
/usr/share/hol-light/Help/theorems.doc
/usr/share/hol-light/Help/thm_frees.doc
/usr/share/hol-light/Help/time.doc
/usr/share/hol-light/Help/tl.doc
/usr/share/hol-light/Help/top_goal.doc
/usr/share/hol-light/Help/top_realgoal.doc
/usr/share/hol-light/Help/top_thm.doc
/usr/share/hol-light/Help/try_user_parser.doc
/usr/share/hol-light/Help/try_user_printer.doc
/usr/share/hol-light/Help/tryapplyd.doc
/usr/share/hol-light/Help/tryfind.doc
/usr/share/hol-light/Help/type_abbrevs.doc
/usr/share/hol-light/Help/type_invention_error.doc
/usr/share/hol-light/Help/type_invention_warning.doc
/usr/share/hol-light/Help/type_match.doc
/usr/share/hol-light/Help/type_of.doc
/usr/share/hol-light/Help/type_of_pretype.doc
/usr/share/hol-light/Help/type_subst.doc
/usr/share/hol-light/Help/type_vars_in_term.doc
/usr/share/hol-light/Help/types.doc
/usr/share/hol-light/Help/typify_universal_set.doc
/usr/share/hol-light/Help/tysubst.doc
/usr/share/hol-light/Help/tyvars.doc
/usr/share/hol-light/Help/uncurry.doc
/usr/share/hol-light/Help/undefine.doc
/usr/share/hol-light/Help/undefined.doc
/usr/share/hol-light/Help/unhide_constant.doc
/usr/share/hol-light/Help/union.doc
/usr/share/hol-light/Help/union_prime.doc
/usr/share/hol-light/Help/unions.doc
/usr/share/hol-light/Help/unions_prime.doc
/usr/share/hol-light/Help/uniq.doc
/usr/share/hol-light/Help/unparse_as_binder.doc
/usr/share/hol-light/Help/unparse_as_infix.doc
/usr/share/hol-light/Help/unparse_as_prefix.doc
/usr/share/hol-light/Help/unreserve_words.doc
/usr/share/hol-light/Help/unspaced_binops.doc
/usr/share/hol-light/Help/unzip.doc
/usr/share/hol-light/Help/use_file.doc
/usr/share/hol-light/Help/variables.doc
/usr/share/hol-light/Help/variant.doc
/usr/share/hol-light/Help/variants.doc
/usr/share/hol-light/Help/verbose.doc
/usr/share/hol-light/Help/vfree_in.doc
/usr/share/hol-light/Help/vsubst.doc
/usr/share/hol-light/Help/warn.doc
/usr/share/hol-light/Help/zip.doc
/usr/share/hol-light/IEEE/README
/usr/share/hol-light/IEEE/common.hl
/usr/share/hol-light/IEEE/fixed.hl
/usr/share/hol-light/IEEE/fixed_thms.hl
/usr/share/hol-light/IEEE/float.hl
/usr/share/hol-light/IEEE/float_thms.hl
/usr/share/hol-light/IEEE/ieee.hl
/usr/share/hol-light/IEEE/ieee_thms.hl
/usr/share/hol-light/IEEE/make.ml
/usr/share/hol-light/IsabelleLight/README
/usr/share/hol-light/IsabelleLight/isalight.ml
/usr/share/hol-light/IsabelleLight/make.ml
/usr/share/hol-light/IsabelleLight/meta_rules.ml
/usr/share/hol-light/IsabelleLight/new_tactics.ml
/usr/share/hol-light/IsabelleLight/support.ml
/usr/share/hol-light/Jordan/float.ml
/usr/share/hol-light/Jordan/jordan_curve_theorem.ml
/usr/share/hol-light/Jordan/lib_ext.ml
/usr/share/hol-light/Jordan/make.ml
/usr/share/hol-light/Jordan/metric_spaces.ml
/usr/share/hol-light/Jordan/misc_defs_and_lemmas.ml
/usr/share/hol-light/Jordan/num_ext_gcd.ml
/usr/share/hol-light/Jordan/num_ext_nabs.ml
/usr/share/hol-light/Jordan/parse_ext_override_interface.ml
/usr/share/hol-light/Jordan/real_ext.ml
/usr/share/hol-light/Jordan/real_ext_geom_series.ml
/usr/share/hol-light/Jordan/tactics_ext.ml
/usr/share/hol-light/Jordan/tactics_ext2.ml
/usr/share/hol-light/Jordan/tactics_fix.ml
/usr/share/hol-light/Jordan/tactics_refine.ml
/usr/share/hol-light/LP_arith/Makefile
/usr/share/hol-light/LP_arith/README
/usr/share/hol-light/LP_arith/cdd_cert.c
/usr/share/hol-light/LP_arith/lp_arith.ml
/usr/share/hol-light/LP_arith/lp_tests.ml
/usr/share/hol-light/LP_arith/make.ml
/usr/share/hol-light/Library/agm.ml
/usr/share/hol-light/Library/analysis.ml
/usr/share/hol-light/Library/binary.ml
/usr/share/hol-light/Library/binomial.ml
/usr/share/hol-light/Library/calc_real.ml
/usr/share/hol-light/Library/card.ml
/usr/share/hol-light/Library/floor.ml
/usr/share/hol-light/Library/integer.ml
/usr/share/hol-light/Library/isum.ml
/usr/share/hol-light/Library/iter.ml
/usr/share/hol-light/Library/multiplicative.ml
/usr/share/hol-light/Library/permutations.ml
/usr/share/hol-light/Library/pocklington.ml
/usr/share/hol-light/Library/poly.ml
/usr/share/hol-light/Library/pratt.ml
/usr/share/hol-light/Library/prime.ml
/usr/share/hol-light/Library/primitive.ml
/usr/share/hol-light/Library/products.ml
/usr/share/hol-light/Library/q.ml
/usr/share/hol-light/Library/rstc.ml
/usr/share/hol-light/Library/transc.ml
/usr/share/hol-light/Library/wo.ml
/usr/share/hol-light/Minisat/CREDITS
/usr/share/hol-light/Minisat/README
/usr/share/hol-light/Minisat/dimacs_tools.ml
/usr/share/hol-light/Minisat/make.ml
/usr/share/hol-light/Minisat/minisat_parse.ml
/usr/share/hol-light/Minisat/minisat_prove.ml
/usr/share/hol-light/Minisat/minisat_resolve.ml
/usr/share/hol-light/Minisat/sat_common_tools.ml
/usr/share/hol-light/Minisat/sat_script.ml
/usr/share/hol-light/Minisat/sat_solvers.ml
/usr/share/hol-light/Minisat/sat_tools.ml
/usr/share/hol-light/Minisat/taut.ml
/usr/share/hol-light/Minisat/zc2mso/README
/usr/share/hol-light/Minisat/zc2mso/zc2mso.C
/usr/share/hol-light/Mizarlight/Makefile
/usr/share/hol-light/Mizarlight/duality.ml
/usr/share/hol-light/Mizarlight/duality_holby.ml
/usr/share/hol-light/Mizarlight/make.ml
/usr/share/hol-light/Mizarlight/miz2a.ml
/usr/share/hol-light/Mizarlight/pa_f.ml
/usr/share/hol-light/Model/make.ml
/usr/share/hol-light/Model/modelset.ml
/usr/share/hol-light/Model/semantics.ml
/usr/share/hol-light/Model/syntax.ml
/usr/share/hol-light/Multivariate/canal.ml
/usr/share/hol-light/Multivariate/cauchy.ml
/usr/share/hol-light/Multivariate/clifford.ml
/usr/share/hol-light/Multivariate/complex_database.ml
/usr/share/hol-light/Multivariate/complexes.ml
/usr/share/hol-light/Multivariate/convex.ml
/usr/share/hol-light/Multivariate/cross.ml
/usr/share/hol-light/Multivariate/cvectors.ml
/usr/share/hol-light/Multivariate/degree.ml
/usr/share/hol-light/Multivariate/derivatives.ml
/usr/share/hol-light/Multivariate/determinants.ml
/usr/share/hol-light/Multivariate/flyspeck.ml
/usr/share/hol-light/Multivariate/gamma.ml
/usr/share/hol-light/Multivariate/geom.ml
/usr/share/hol-light/Multivariate/integration.ml
/usr/share/hol-light/Multivariate/lpspaces.ml
/usr/share/hol-light/Multivariate/make.ml
/usr/share/hol-light/Multivariate/make_complex.ml
/usr/share/hol-light/Multivariate/measure.ml
/usr/share/hol-light/Multivariate/metric.ml
/usr/share/hol-light/Multivariate/misc.ml
/usr/share/hol-light/Multivariate/moretop.ml
/usr/share/hol-light/Multivariate/multivariate_database.ml
/usr/share/hol-light/Multivariate/paths.ml
/usr/share/hol-light/Multivariate/polytope.ml
/usr/share/hol-light/Multivariate/realanalysis.ml
/usr/share/hol-light/Multivariate/tarski.ml
/usr/share/hol-light/Multivariate/topology.ml
/usr/share/hol-light/Multivariate/transcendentals.ml
/usr/share/hol-light/Multivariate/vectors.ml
/usr/share/hol-light/Multivariate/wlog.ml
/usr/share/hol-light/Multivariate/wlog_examples.ml
/usr/share/hol-light/Ntrie/ntrie.ml
/usr/share/hol-light/Ntrie/ntrie_tests.ml
/usr/share/hol-light/Permutation/DOC.txt
/usr/share/hol-light/Permutation/make.ml
/usr/share/hol-light/Permutation/morelist.ml
/usr/share/hol-light/Permutation/nummax.ml
/usr/share/hol-light/Permutation/permutation.ml
/usr/share/hol-light/Permutation/permuted.ml
/usr/share/hol-light/Permutation/qsort.ml
/usr/share/hol-light/Proofrecording/README
/usr/share/hol-light/Proofrecording/diffs/basics.ml
/usr/share/hol-light/Proofrecording/diffs/bool.ml
/usr/share/hol-light/Proofrecording/diffs/depgraph.ml
/usr/share/hol-light/Proofrecording/diffs/equal.ml
/usr/share/hol-light/Proofrecording/diffs/hol.ml
/usr/share/hol-light/Proofrecording/diffs/proofobjects_coq.ml
/usr/share/hol-light/Proofrecording/diffs/proofobjects_dummy.ml
/usr/share/hol-light/Proofrecording/diffs/proofobjects_init.ml
/usr/share/hol-light/Proofrecording/diffs/proofobjects_trt.ml
/usr/share/hol-light/Proofrecording/diffs/tactics.ml
/usr/share/hol-light/Proofrecording/diffs/thm.ml
/usr/share/hol-light/Proofrecording/hol_light/Help
/usr/share/hol-light/Proofrecording/hol_light/Makefile
/usr/share/hol-light/Proofrecording/tools/Makefile
/usr/share/hol-light/Proofrecording/tools/detecteq_readme.txt
/usr/share/hol-light/Proofrecording/tools/init.ml
/usr/share/hol-light/Proofrecording/tools/startcore.ml
/usr/share/hol-light/Proofrecording/tools/src/DetectEq.java
/usr/share/hol-light/Proofrecording/tools/src/NamedTheorem.java
/usr/share/hol-light/QBF/README
/usr/share/hol-light/QBF/make.ml
/usr/share/hol-light/QBF/mygraph.ml
/usr/share/hol-light/QBF/qbf.ml
/usr/share/hol-light/QBF/qbfr.ml
/usr/share/hol-light/Quaternions/make.ml
/usr/share/hol-light/Quaternions/misc.hl
/usr/share/hol-light/Quaternions/qanal.hl
/usr/share/hol-light/Quaternions/qcalc.hl
/usr/share/hol-light/Quaternions/qderivative.hl
/usr/share/hol-light/Quaternions/qisom.hl
/usr/share/hol-light/Quaternions/qnormalizer.hl
/usr/share/hol-light/Quaternions/quaternion.hl
/usr/share/hol-light/RichterHilbertAxiomGeometry/HilbertAxiom_read.ml
/usr/share/hol-light/RichterHilbertAxiomGeometry/README
/usr/share/hol-light/RichterHilbertAxiomGeometry/TarskiAxiomGeometry_read.ml
/usr/share/hol-light/RichterHilbertAxiomGeometry/Topology.ml
/usr/share/hol-light/RichterHilbertAxiomGeometry/UniversalPropCartProd.ml
/usr/share/hol-light/RichterHilbertAxiomGeometry/error-checking.ml
/usr/share/hol-light/RichterHilbertAxiomGeometry/from_topology.ml
/usr/share/hol-light/RichterHilbertAxiomGeometry/inverse_bug_puzzle_read.ml
/usr/share/hol-light/RichterHilbertAxiomGeometry/readable.ml
/usr/share/hol-light/RichterHilbertAxiomGeometry/thmFontHilbertAxiom
/usr/share/hol-light/RichterHilbertAxiomGeometry/thmFontHilbertAxiom.ml
/usr/share/hol-light/RichterHilbertAxiomGeometry/thmTopology
/usr/share/hol-light/RichterHilbertAxiomGeometry/miz3/FontHilbertAxiom.ml
/usr/share/hol-light/RichterHilbertAxiomGeometry/miz3/HilbertAxiom.ml
/usr/share/hol-light/RichterHilbertAxiomGeometry/miz3/Miz3Tips
/usr/share/hol-light/RichterHilbertAxiomGeometry/miz3/README
/usr/share/hol-light/RichterHilbertAxiomGeometry/miz3/hol-light-fonts.el
/usr/share/hol-light/RichterHilbertAxiomGeometry/miz3/hol-light-fonts.elc
/usr/share/hol-light/RichterHilbertAxiomGeometry/miz3/make.ml
/usr/share/hol-light/Rqe/asym.ml
/usr/share/hol-light/Rqe/basic.ml
/usr/share/hol-light/Rqe/condense.ml
/usr/share/hol-light/Rqe/condense_thms.ml
/usr/share/hol-light/Rqe/dedmatrix.ml
/usr/share/hol-light/Rqe/dedmatrix_thms.ml
/usr/share/hol-light/Rqe/defs.ml
/usr/share/hol-light/Rqe/examples.ml
/usr/share/hol-light/Rqe/inferisign.ml
/usr/share/hol-light/Rqe/inferisign_thms.ml
/usr/share/hol-light/Rqe/inferpsign.ml
/usr/share/hol-light/Rqe/inferpsign_thms.ml
/usr/share/hol-light/Rqe/lift_qelim.ml
/usr/share/hol-light/Rqe/list_rewrites.ml
/usr/share/hol-light/Rqe/main_thms.ml
/usr/share/hol-light/Rqe/make.ml
/usr/share/hol-light/Rqe/matinsert.ml
/usr/share/hol-light/Rqe/matinsert_thms.ml
/usr/share/hol-light/Rqe/num_calc_simp.ml
/usr/share/hol-light/Rqe/pdivides.ml
/usr/share/hol-light/Rqe/pdivides_thms.ml
/usr/share/hol-light/Rqe/poly_ext.ml
/usr/share/hol-light/Rqe/rewrites.ml
/usr/share/hol-light/Rqe/rol.ml
/usr/share/hol-light/Rqe/rqe_lib.ml
/usr/share/hol-light/Rqe/rqe_list.ml
/usr/share/hol-light/Rqe/rqe_main.ml
/usr/share/hol-light/Rqe/rqe_num.ml
/usr/share/hol-light/Rqe/rqe_real.ml
/usr/share/hol-light/Rqe/rqe_tactics_ext.ml
/usr/share/hol-light/Rqe/signs.ml
/usr/share/hol-light/Rqe/signs_thms.ml
/usr/share/hol-light/Rqe/simplify.ml
/usr/share/hol-light/Rqe/testform.ml
/usr/share/hol-light/Rqe/testform_thms.ml
/usr/share/hol-light/Rqe/timers.ml
/usr/share/hol-light/Rqe/util.ml
/usr/share/hol-light/Rqe/work_thms.ml
/usr/share/hol-light/Tutorial/Abstractions_and_quantifiers.ml
/usr/share/hol-light/Tutorial/Changing_proof_style.ml
/usr/share/hol-light/Tutorial/Custom_inference_rules.ml
/usr/share/hol-light/Tutorial/Custom_tactics.ml
/usr/share/hol-light/Tutorial/Defining_new_types.ml
/usr/share/hol-light/Tutorial/Embedding_of_logics_deep.ml
/usr/share/hol-light/Tutorial/Embedding_of_logics_shallow.ml
/usr/share/hol-light/Tutorial/HOL_as_a_functional_programming_language.ml
/usr/share/hol-light/Tutorial/HOL_basics.ml
/usr/share/hol-light/Tutorial/HOLs_number_systems.ml
/usr/share/hol-light/Tutorial/Inductive_datatypes.ml
/usr/share/hol-light/Tutorial/Inductive_definitions.ml
/usr/share/hol-light/Tutorial/Linking_external_tools.ml
/usr/share/hol-light/Tutorial/Number_theory.ml
/usr/share/hol-light/Tutorial/Propositional_logic.ml
/usr/share/hol-light/Tutorial/Real_analysis.ml
/usr/share/hol-light/Tutorial/Recursive_definitions.ml
/usr/share/hol-light/Tutorial/Semantics_of_programming_languages_deep.ml
/usr/share/hol-light/Tutorial/Semantics_of_programming_languages_shallow.ml
/usr/share/hol-light/Tutorial/Sets_and_functions.ml
/usr/share/hol-light/Tutorial/Tactics_and_tacticals.ml
/usr/share/hol-light/Tutorial/Vectors.ml
/usr/share/hol-light/Tutorial/Wellfounded_induction.ml
/usr/share/hol-light/Tutorial/all.ml
/usr/share/hol-light/Unity/README
/usr/share/hol-light/Unity/aux_definitions.ml
/usr/share/hol-light/Unity/make.ml
/usr/share/hol-light/Unity/mk_comp_unity.ml
/usr/share/hol-light/Unity/mk_ensures.ml
/usr/share/hol-light/Unity/mk_gen_induct.ml
/usr/share/hol-light/Unity/mk_leadsto.ml
/usr/share/hol-light/Unity/mk_state_logic.ml
/usr/share/hol-light/Unity/mk_unity_prog.ml
/usr/share/hol-light/Unity/mk_unless.ml
/usr/share/hol-light/miz3/ERRORS
/usr/share/hol-light/miz3/README
/usr/share/hol-light/miz3/exrc
/usr/share/hol-light/miz3/make.ml
/usr/share/hol-light/miz3/miz3.ml
/usr/share/hol-light/miz3/miz3_of_hol.ml
/usr/share/hol-light/miz3/test.ml
/usr/share/hol-light/miz3/Samples/NEEDS
/usr/share/hol-light/miz3/Samples/bug0.ml
/usr/share/hol-light/miz3/Samples/bug1.ml
/usr/share/hol-light/miz3/Samples/bug2.ml
/usr/share/hol-light/miz3/Samples/bug3.ml
/usr/share/hol-light/miz3/Samples/drinker.ml
/usr/share/hol-light/miz3/Samples/forster.ml
/usr/share/hol-light/miz3/Samples/icms.ml
/usr/share/hol-light/miz3/Samples/irrat2.ml
/usr/share/hol-light/miz3/Samples/lagrange.ml
/usr/share/hol-light/miz3/Samples/lagrange1.ml
/usr/share/hol-light/miz3/Samples/luxury.ml
/usr/share/hol-light/miz3/Samples/other_mizs.ml
/usr/share/hol-light/miz3/Samples/robbins.ml
/usr/share/hol-light/miz3/Samples/sample.ml
/usr/share/hol-light/miz3/Samples/samples.ml
/usr/share/hol-light/miz3/Samples/talk.ml
/usr/share/hol-light/miz3/Samples/tobias.ml
/usr/share/hol-light/miz3/Samples/wishes.ml
/usr/share/hol-light/miz3/bin/miz3
/usr/share/hol-light/miz3/bin/miz3e
/usr/share/hol-light/miz3/bin/miz3f
/usr/share/hol-light/miz3/grammar/miz3.y
/usr/share/lintian/overrides/hol-light
/usr/share/man/man1/hol-light.1.gz
/usr/share/menu/hol-light
/var/lib/ocaml/lintian/hol-light.info
/var/lib/ocaml/md5sums/hol-light.md5sums

Changelog

2017-01-09 - Hendrik Tews <hendrik@askra.de>
hol-light (20170109-1) unstable; urgency=low
[ Mehdi Dogguy ]
* Update watch file
[ Hendrik Tews ]
* Imported Upstream version 20170109
with git hash f468686c09996f77ccfa98c30ba98f8db2c8cfd9
* update copyright, patches, README.Debian
* standards-version 3.9.8; update Vcs fields
* disable building the Mizarlight syntax extension (fails upstream with
OCaml 4.02 - already reported to John Harrison)
* clear exec bit fix on RichterHilbertAxiomGeometry/Topology.ml (fixed
upstream)
* add exec bit fixes for Help/HYP_TAC.doc,
RichterHilbertAxiomGeometry/TarskiAxiomGeometry_read.ml and
Multivariate/cvectors.ml
* don't install jar files in Proofrecording/tools
* add patch cd-holtest-parallel to fix current directory in parallel
test
2013-11-10 - Hendrik Tews <hendrik@askra.de>
hol-light (20131026-1) unstable; urgency=low
* new upstream version revision 177 from 2013-10-26
* use new pa_j and adjust camlp5 dependencies
* delete executable bit of RichterHilbertAxiomGeometry/Topology.ml 
during installation
2013-08-14 - Hendrik Tews <hendrik@askra.de>
hol-light (20130811-1) unstable; urgency=low
* new upstream version revision 170 from 2013-08-11
* fix vcs fields
* refresh patches
* delete include-compiler-libs patch (applied upstream)
* update elc file path in hol-light-source.exclude
* update copyright
2013-05-17 - Hendrik Tews <hendrik@askra.de>
hol-light (20130511-1) unstable; urgency=low
* new upstream version revision 162 from 2013-05-11
* fix typo in package description (Closes: #680494)
* set prioity to extra
* omit new elc file from package
* adapt copyright info
* add new patch include-compiler-libs for OCaml 4 compatibility
* bump to standards version 3.9.4
* improve debian readme
2012-06-10 - Hendrik Tews <hendrik@askra.de>
hol-light (20120602-1) unstable; urgency=low
* new upstream version revision 146 from 2012-06-02
* remove holtest-dependency-hint patch
* refresh remaining patches
2012-05-31 - Hendrik Tews <hendrik@askra.de>
hol-light (20120530-1) unstable; urgency=low
* new upstream version revision 141 from 2012-05-30
* remove patches that have been applied upstream:
adapt-holtest-for-debian and pa-j-makefile-fix
* adapt debian/copyright
* simplify debian/rules
* add patch holtest-dependency-hint
2012-04-24 - Hendrik Tews <hendrik@askra.de>
hol-light (20120423-1) unstable; urgency=low
* Initial release (Closes: #663754)

See Also

Package Description
hol88-contrib-help_2.02.19940316-33_all.deb Higher Order Logic, user contributed online help files
hol88-contrib-source_2.02.19940316-33_all.deb Higher Order Logic, user contributed source
hol88-doc_2.02.19940316-33_all.deb Documentation for hol88
hol88-help_2.02.19940316-33_all.deb Higher Order Logic, online help files
hol88-library-help_2.02.19940316-33_all.deb Higher Order Logic, library online help files
hol88-library-source_2.02.19940316-33_all.deb Higher Order Logic, library source files
hol88-library_2.02.19940316-33_amd64.deb Higher Order Logic, binary library modules
hol88-source_2.02.19940316-33_all.deb Higher Order Logic, source files
hol88_2.02.19940316-33_amd64.deb Higher Order Logic, system image
holdingnuts-server_0.0.5-4_amd64.deb poker server
holdingnuts_0.0.5-4_amd64.deb poker client
holotz-castle-data_1.3.14-9_all.deb platform game with high doses of mystery - data files
holotz-castle-editor_1.3.14-9_amd64.deb platform game with high doses of mystery - level editor
holotz-castle_1.3.14-9_amd64.deb platform game with high doses of mystery
homebank-data_5.0.9-1_all.deb Data files for homebank
Advertisement
Advertisement