Package - hol-light

Package: hol-light
apt-get install hol-light

Manuals in package:

hol-light(1)

Documentations in package:

hol-light

Primary informations

Download package: http://deb.debian.org/debian/pool/main/h/hol-light/hol-light_3.0.0-2+b7_amd64.deb (Size: 5.7MiB)

Property	Value
Package	hol-light
Source	hol-light (1:3.0.0-2)
Version	1:3.0.0-2+b7
Installed-Size	46111
Maintainer	Debian OCaml Maintainers
Architecture	amd64
Depends	camlp5, camlp5-4new7, libcamlp-streams-ocaml-dev-0lin0, libcompiler-libs-ocaml-dev-4b6d0, libstdlib-ocaml-dev-m4xw9, libzarith-ocaml-dev-h79v1, ocaml-5.3.0
Suggests	readline-editor, prover9, coinor-csdp, pari-gp, maxima, dmtcp, libocamlgraph-ocaml-dev, python
Description	HOL Light theorem prover
Description-md5	4a69d13e99a5d21da7555a1ffc45abd5
Homepage	https://www.cl.cam.ac.uk/~jrh13/hol-light/
Section	math
Priority	optional
Filename	pool/main/h/hol-light/hol-light_3.0.0-2+b7_amd64.deb
Size	6000992
MD5sum	8b9f707617bfa7895af18600fd668562
SHA256	c5925927be57c9e4a3357b61d126af5bfa9a760beb743f5dcc611224993053b4

Files in package

/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.amd64.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/.github/workflows/main.yml
/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/isoperimetric.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/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/Boyer_Moore/waterfall.ml
/usr/share/hol-light/Cadical/README
/usr/share/hol-light/Cadical/cadical.ml
/usr/share/hol-light/Cadical/cnf.ml
/usr/share/hol-light/Cadical/dimacs.ml
/usr/share/hol-light/Cadical/ldrup.ml
/usr/share/hol-light/Cadical/make.ml
/usr/share/hol-light/Cadical/test.ml
/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/Divstep/Makefile
/usr/share/hol-light/Divstep/README
/usr/share/hol-light/Divstep/divstep.ml
/usr/share/hol-light/Divstep/divstep_bounds.ml
/usr/share/hol-light/Divstep/hull-light-20230416.sage
/usr/share/hol-light/Divstep/hull_light.ml
/usr/share/hol-light/Divstep/idivstep.ml
/usr/share/hol-light/Divstep/make.ml
/usr/share/hol-light/EC/README
/usr/share/hol-light/EC/ccsm2.ml
/usr/share/hol-light/EC/computegroup.ml
/usr/share/hol-light/EC/curve25519.ml
/usr/share/hol-light/EC/edmont.ml
/usr/share/hol-light/EC/edwards.ml
/usr/share/hol-light/EC/edwards25519.ml
/usr/share/hol-light/EC/edwards448.ml
/usr/share/hol-light/EC/excluderoots.ml
/usr/share/hol-light/EC/exprojective.ml
/usr/share/hol-light/EC/family25519.ml
/usr/share/hol-light/EC/formulary_jacobian.ml
/usr/share/hol-light/EC/formulary_projective.ml
/usr/share/hol-light/EC/formulary_xzprojective.ml
/usr/share/hol-light/EC/jacobian.ml
/usr/share/hol-light/EC/make.ml
/usr/share/hol-light/EC/misc.ml
/usr/share/hol-light/EC/montgomery.ml
/usr/share/hol-light/EC/montwe.ml
/usr/share/hol-light/EC/nistp192.ml
/usr/share/hol-light/EC/nistp224.ml
/usr/share/hol-light/EC/nistp256.ml
/usr/share/hol-light/EC/nistp384.ml
/usr/share/hol-light/EC/nistp521.ml
/usr/share/hol-light/EC/projective.ml
/usr/share/hol-light/EC/secp192k1.ml
/usr/share/hol-light/EC/secp224k1.ml
/usr/share/hol-light/EC/secp256k1.ml
/usr/share/hol-light/EC/wei25519.ml
/usr/share/hol-light/EC/weierstrass.ml
/usr/share/hol-light/EC/x25519.ml
/usr/share/hol-light/EC/xzprojective.ml
/usr/share/hol-light/Examples/bdd_examples.ml
/usr/share/hol-light/Examples/bitblast.ml
/usr/share/hol-light/Examples/bondy.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/complexpolygon.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/digit_serial_methods.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/miller_rabin.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/padics.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/pseudoprime.ml
/usr/share/hol-light/Examples/rectypes.ml
/usr/share/hol-light/Examples/reduct.ml
/usr/share/hol-light/Examples/safetyliveness.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/Examples/zolotarev.ml
/usr/share/hol-light/Formal_ineqs/README.md
/usr/share/hol-light/Formal_ineqs/arith/arith_cache.hl
/usr/share/hol-light/Formal_ineqs/arith/arith_float.hl
/usr/share/hol-light/Formal_ineqs/arith/arith_nat.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_pow.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/num_exp_theory.hl
/usr/share/hol-light/Formal_ineqs/arith_options.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/examples.hl
/usr/share/hol-light/Formal_ineqs/examples_flyspeck.hl
/usr/share/hol-light/Formal_ineqs/examples_other.hl
/usr/share/hol-light/Formal_ineqs/examples_poly.hl
/usr/share/hol-light/Formal_ineqs/informal/informal_asn_acs.hl
/usr/share/hol-light/Formal_ineqs/informal/informal_atn.hl
/usr/share/hol-light/Formal_ineqs/informal/informal_eval_interval.hl
/usr/share/hol-light/Formal_ineqs/informal/informal_exp.hl
/usr/share/hol-light/Formal_ineqs/informal/informal_float.hl
/usr/share/hol-light/Formal_ineqs/informal/informal_interval.hl
/usr/share/hol-light/Formal_ineqs/informal/informal_log.hl
/usr/share/hol-light/Formal_ineqs/informal/informal_matan.hl
/usr/share/hol-light/Formal_ineqs/informal/informal_nat.hl
/usr/share/hol-light/Formal_ineqs/informal/informal_poly.hl
/usr/share/hol-light/Formal_ineqs/informal/informal_search.hl
/usr/share/hol-light/Formal_ineqs/informal/informal_sin_cos.hl
/usr/share/hol-light/Formal_ineqs/informal/informal_taylor.hl
/usr/share/hol-light/Formal_ineqs/informal/informal_verifier.hl
/usr/share/hol-light/Formal_ineqs/lib/ipow.hl
/usr/share/hol-light/Formal_ineqs/lib/ssrbool.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/lib/ssrfun.hl
/usr/share/hol-light/Formal_ineqs/lib/ssrnat.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/make.ml
/usr/share/hol-light/Formal_ineqs/misc/misc_functions.hl
/usr/share/hol-light/Formal_ineqs/misc/misc_vars.hl
/usr/share/hol-light/Formal_ineqs/misc/report.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/tests/data/gen_nat_data.py
/usr/share/hol-light/Formal_ineqs/tests/float_data.hl
/usr/share/hol-light/Formal_ineqs/tests/log.hl
/usr/share/hol-light/Formal_ineqs/tests/nat_test.hl
/usr/share/hol-light/Formal_ineqs/tests/results.hl
/usr/share/hol-light/Formal_ineqs/tests/test_utils.hl
/usr/share/hol-light/Formal_ineqs/trig/asn_acs_eval.hl
/usr/share/hol-light/Formal_ineqs/trig/atn.hl
/usr/share/hol-light/Formal_ineqs/trig/atn_eval.hl
/usr/share/hol-light/Formal_ineqs/trig/cos_bounds_eval.hl
/usr/share/hol-light/Formal_ineqs/trig/cos_eval.hl
/usr/share/hol-light/Formal_ineqs/trig/exp_eval.hl
/usr/share/hol-light/Formal_ineqs/trig/exp_log.hl
/usr/share/hol-light/Formal_ineqs/trig/log_eval.hl
/usr/share/hol-light/Formal_ineqs/trig/matan.hl
/usr/share/hol-light/Formal_ineqs/trig/matan_eval.hl
/usr/share/hol-light/Formal_ineqs/trig/poly.hl
/usr/share/hol-light/Formal_ineqs/trig/poly_eval.hl
/usr/share/hol-light/Formal_ineqs/trig/series.hl
/usr/share/hol-light/Formal_ineqs/trig/sin_cos.hl
/usr/share/hol-light/Formal_ineqs/trig/sin_eval.hl
/usr/share/hol-light/Formal_ineqs/trig/test.hl
/usr/share/hol-light/Formal_ineqs/trig/unused.hl
/usr/share/hol-light/Formal_ineqs/update_paths.py
/usr/share/hol-light/Formal_ineqs/verifier/certificate.hl
/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_options.hl
/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/GL/COPYING
/usr/share/hol-light/GL/README.md
/usr/share/hol-light/GL/completeness.ml
/usr/share/hol-light/GL/decid.ml
/usr/share/hol-light/GL/gl.ml
/usr/share/hol-light/GL/k4lr.ml
/usr/share/hol-light/GL/make.ml
/usr/share/hol-light/GL/misc.ml
/usr/share/hol-light/GL/modal.ml
/usr/share/hol-light/GL/tests.ml
/usr/share/hol-light/Geometric_Algebra/README
/usr/share/hol-light/Geometric_Algebra/geometricalgebra.ml
/usr/share/hol-light/Geometric_Algebra/make.ml
/usr/share/hol-light/Geometric_Algebra/quaternions.ml
/usr/share/hol-light/Help/.joinparsers.hlp
/usr/share/hol-light/Help/.orparser.hlp
/usr/share/hol-light/Help/.pipeparser.hlp
/usr/share/hol-light/Help/.singlefun.hlp
/usr/share/hol-light/Help/.upto.hlp
/usr/share/hol-light/Help/.valmod.hlp
/usr/share/hol-light/Help/ABBREV_TAC.hlp
/usr/share/hol-light/Help/ABS.hlp
/usr/share/hol-light/Help/ABS_CONV.hlp
/usr/share/hol-light/Help/ABS_TAC.hlp
/usr/share/hol-light/Help/AC.hlp
/usr/share/hol-light/Help/ACCEPT_TAC.hlp
/usr/share/hol-light/Help/ADD_ASSUM.hlp
/usr/share/hol-light/Help/ALL_CONV.hlp
/usr/share/hol-light/Help/ALL_TAC.hlp
/usr/share/hol-light/Help/ALL_THEN.hlp
/usr/share/hol-light/Help/ALPHA_CONV.hlp
/usr/share/hol-light/Help/ALPHA_UPPERCASE.hlp
/usr/share/hol-light/Help/ANTE_RES_THEN.hlp
/usr/share/hol-light/Help/ANTS_TAC.hlp
/usr/share/hol-light/Help/AP_TERM.hlp
/usr/share/hol-light/Help/AP_TERM_TAC.hlp
/usr/share/hol-light/Help/AP_THM.hlp
/usr/share/hol-light/Help/AP_THM_TAC.hlp
/usr/share/hol-light/Help/ARITH_RULE.hlp
/usr/share/hol-light/Help/ARITH_TAC.hlp
/usr/share/hol-light/Help/ASM.hlp
/usr/share/hol-light/Help/ASM_ARITH_TAC.hlp
/usr/share/hol-light/Help/ASM_CASES_TAC.hlp
/usr/share/hol-light/Help/ASM_FOL_TAC.hlp
/usr/share/hol-light/Help/ASM_INT_ARITH_TAC.hlp
/usr/share/hol-light/Help/ASM_MESON_TAC.hlp
/usr/share/hol-light/Help/ASM_METIS_TAC.hlp
/usr/share/hol-light/Help/ASM_REAL_ARITH_TAC.hlp
/usr/share/hol-light/Help/ASM_REWRITE_RULE.hlp
/usr/share/hol-light/Help/ASM_REWRITE_TAC.hlp
/usr/share/hol-light/Help/ASM_SIMP_TAC.hlp
/usr/share/hol-light/Help/ASSOC_CONV.hlp
/usr/share/hol-light/Help/ASSUME.hlp
/usr/share/hol-light/Help/ASSUME_TAC.hlp
/usr/share/hol-light/Help/ASSUM_LIST.hlp
/usr/share/hol-light/Help/AUGMENT_SIMPSET.hlp
/usr/share/hol-light/Help/BETA.hlp
/usr/share/hol-light/Help/BETAS_CONV.hlp
/usr/share/hol-light/Help/BETA_CONV.hlp
/usr/share/hol-light/Help/BETA_RULE.hlp
/usr/share/hol-light/Help/BETA_TAC.hlp
/usr/share/hol-light/Help/BINDER_CONV.hlp
/usr/share/hol-light/Help/BINOP2_CONV.hlp
/usr/share/hol-light/Help/BINOP_CONV.hlp
/usr/share/hol-light/Help/BINOP_TAC.hlp
/usr/share/hol-light/Help/BITS_ELIM_CONV.hlp
/usr/share/hol-light/Help/BOOL_CASES_TAC.hlp
/usr/share/hol-light/Help/C.hlp
/usr/share/hol-light/Help/CACHE_CONV.hlp
/usr/share/hol-light/Help/CASE_REWRITE_TAC.hlp
/usr/share/hol-light/Help/CCONTR.hlp
/usr/share/hol-light/Help/CHANGED_CONV.hlp
/usr/share/hol-light/Help/CHANGED_TAC.hlp
/usr/share/hol-light/Help/CHAR_EQ_CONV.hlp
/usr/share/hol-light/Help/CHEAT_TAC.hlp
/usr/share/hol-light/Help/CHOOSE_TAC.hlp
/usr/share/hol-light/Help/CHOOSE_THEN.hlp
/usr/share/hol-light/Help/CHOOSE_UPPERCASE.hlp
/usr/share/hol-light/Help/CLAIM_TAC.hlp
/usr/share/hol-light/Help/CNF_CONV.hlp
/usr/share/hol-light/Help/COMB2_CONV.hlp
/usr/share/hol-light/Help/COMB_CONV.hlp
/usr/share/hol-light/Help/CONDS_CELIM_CONV.hlp
/usr/share/hol-light/Help/CONDS_ELIM_CONV.hlp
/usr/share/hol-light/Help/COND_CASES_TAC.hlp
/usr/share/hol-light/Help/COND_ELIM_CONV.hlp
/usr/share/hol-light/Help/CONJ.hlp
/usr/share/hol-light/Help/CONJUNCT1.hlp
/usr/share/hol-light/Help/CONJUNCT2.hlp
/usr/share/hol-light/Help/CONJUNCTS_THEN.hlp
/usr/share/hol-light/Help/CONJUNCTS_THEN2.hlp
/usr/share/hol-light/Help/CONJUNCTS_UPPERCASE.hlp
/usr/share/hol-light/Help/CONJ_ACI_RULE.hlp
/usr/share/hol-light/Help/CONJ_CANON_CONV.hlp
/usr/share/hol-light/Help/CONJ_PAIR.hlp
/usr/share/hol-light/Help/CONJ_TAC.hlp
/usr/share/hol-light/Help/CONTR.hlp
/usr/share/hol-light/Help/CONTRAPOS_CONV.hlp
/usr/share/hol-light/Help/CONTR_TAC.hlp
/usr/share/hol-light/Help/CONV_RULE.hlp
/usr/share/hol-light/Help/CONV_TAC.hlp
/usr/share/hol-light/Help/DEDUCT_ANTISYM_RULE.hlp
/usr/share/hol-light/Help/DENUMERAL.hlp
/usr/share/hol-light/Help/DEPTH_BINOP_CONV.hlp
/usr/share/hol-light/Help/DEPTH_CONV.hlp
/usr/share/hol-light/Help/DEPTH_SQCONV.hlp
/usr/share/hol-light/Help/DESTRUCT_TAC.hlp
/usr/share/hol-light/Help/DIMINDEX_CONV.hlp
/usr/share/hol-light/Help/DIMINDEX_TAC.hlp
/usr/share/hol-light/Help/DISCH.hlp
/usr/share/hol-light/Help/DISCH_ALL.hlp
/usr/share/hol-light/Help/DISCH_TAC.hlp
/usr/share/hol-light/Help/DISCH_THEN.hlp
/usr/share/hol-light/Help/DISJ1.hlp
/usr/share/hol-light/Help/DISJ1_TAC.hlp
/usr/share/hol-light/Help/DISJ2.hlp
/usr/share/hol-light/Help/DISJ2_TAC.hlp
/usr/share/hol-light/Help/DISJ_ACI_RULE.hlp
/usr/share/hol-light/Help/DISJ_CANON_CONV.hlp
/usr/share/hol-light/Help/DISJ_CASES.hlp
/usr/share/hol-light/Help/DISJ_CASES_TAC.hlp
/usr/share/hol-light/Help/DISJ_CASES_THEN.hlp
/usr/share/hol-light/Help/DISJ_CASES_THEN2.hlp
/usr/share/hol-light/Help/DNF_CONV.hlp
/usr/share/hol-light/Help/EQF_ELIM.hlp
/usr/share/hol-light/Help/EQF_INTRO.hlp
/usr/share/hol-light/Help/EQT_ELIM.hlp
/usr/share/hol-light/Help/EQT_INTRO.hlp
/usr/share/hol-light/Help/EQ_IMP_RULE.hlp
/usr/share/hol-light/Help/EQ_MP.hlp
/usr/share/hol-light/Help/EQ_TAC.hlp
/usr/share/hol-light/Help/ETA_CONV.hlp
/usr/share/hol-light/Help/EVERY.hlp
/usr/share/hol-light/Help/EVERY_ASSUM.hlp
/usr/share/hol-light/Help/EVERY_CONV.hlp
/usr/share/hol-light/Help/EVERY_TCL.hlp
/usr/share/hol-light/Help/EXISTENCE.hlp
/usr/share/hol-light/Help/EXISTS_EQUATION.hlp
/usr/share/hol-light/Help/EXISTS_TAC.hlp
/usr/share/hol-light/Help/EXISTS_UPPERCASE.hlp
/usr/share/hol-light/Help/EXPAND_CASES_CONV.hlp
/usr/share/hol-light/Help/EXPAND_NSUM_CONV.hlp
/usr/share/hol-light/Help/EXPAND_SUM_CONV.hlp
/usr/share/hol-light/Help/EXPAND_TAC.hlp
/usr/share/hol-light/Help/FAIL_TAC.hlp
/usr/share/hol-light/Help/FIND_ASSUM.hlp
/usr/share/hol-light/Help/FIRST.hlp
/usr/share/hol-light/Help/FIRST_ASSUM.hlp
/usr/share/hol-light/Help/FIRST_CONV.hlp
/usr/share/hol-light/Help/FIRST_TCL.hlp
/usr/share/hol-light/Help/FIRST_X_ASSUM.hlp
/usr/share/hol-light/Help/FIX_TAC.hlp
/usr/share/hol-light/Help/FORALL_UNWIND_CONV.hlp
/usr/share/hol-light/Help/FREEZE_THEN.hlp
/usr/share/hol-light/Help/F_F.hlp
/usr/share/hol-light/Help/GABS_CONV.hlp
/usr/share/hol-light/Help/GEN.hlp
/usr/share/hol-light/Help/GENERAL_REWRITE_CONV.hlp
/usr/share/hol-light/Help/GENL.hlp
/usr/share/hol-light/Help/GEN_ALL.hlp
/usr/share/hol-light/Help/GEN_ALPHA_CONV.hlp
/usr/share/hol-light/Help/GEN_BETA_CONV.hlp
/usr/share/hol-light/Help/GEN_MESON_TAC.hlp
/usr/share/hol-light/Help/GEN_NNF_CONV.hlp
/usr/share/hol-light/Help/GEN_PART_MATCH.hlp
/usr/share/hol-light/Help/GEN_REAL_ARITH.hlp
/usr/share/hol-light/Help/GEN_REWRITE_CONV.hlp
/usr/share/hol-light/Help/GEN_REWRITE_RULE.hlp
/usr/share/hol-light/Help/GEN_REWRITE_TAC.hlp
/usr/share/hol-light/Help/GEN_SIMPLIFY_CONV.hlp
/usr/share/hol-light/Help/GEN_TAC.hlp
/usr/share/hol-light/Help/GSYM.hlp
/usr/share/hol-light/Help/HAS_SIZE_CONV.hlp
/usr/share/hol-light/Help/HAS_SIZE_DIMINDEX_RULE.hlp
/usr/share/hol-light/Help/HIGHER_REWRITE_CONV.hlp
/usr/share/hol-light/Help/HINT_EXISTS_TAC.hlp
/usr/share/hol-light/Help/HYP_TAC.hlp
/usr/share/hol-light/Help/HYP_UPPERCASE.hlp
/usr/share/hol-light/Help/I.hlp
/usr/share/hol-light/Help/IMP_ANTISYM_RULE.hlp
/usr/share/hol-light/Help/IMP_RES_THEN.hlp
/usr/share/hol-light/Help/IMP_REWRITE_TAC.hlp
/usr/share/hol-light/Help/IMP_REWR_CONV.hlp
/usr/share/hol-light/Help/IMP_TRANS.hlp
/usr/share/hol-light/Help/INDUCT_TAC.hlp
/usr/share/hol-light/Help/INSTANTIATE_ALL.hlp
/usr/share/hol-light/Help/INSTANTIATE_UPPERCASE.hlp
/usr/share/hol-light/Help/INST_TYPE.hlp
/usr/share/hol-light/Help/INST_UPPERCASE.hlp
/usr/share/hol-light/Help/INTEGER_RULE.hlp
/usr/share/hol-light/Help/INTEGER_TAC.hlp
/usr/share/hol-light/Help/INTRO_TAC.hlp
/usr/share/hol-light/Help/INT_ABS_CONV.hlp
/usr/share/hol-light/Help/INT_ADD_CONV.hlp
/usr/share/hol-light/Help/INT_ARITH.hlp
/usr/share/hol-light/Help/INT_ARITH_TAC.hlp
/usr/share/hol-light/Help/INT_EQ_CONV.hlp
/usr/share/hol-light/Help/INT_GE_CONV.hlp
/usr/share/hol-light/Help/INT_GT_CONV.hlp
/usr/share/hol-light/Help/INT_LE_CONV.hlp
/usr/share/hol-light/Help/INT_LT_CONV.hlp
/usr/share/hol-light/Help/INT_MAX_CONV.hlp
/usr/share/hol-light/Help/INT_MIN_CONV.hlp
/usr/share/hol-light/Help/INT_MUL_CONV.hlp
/usr/share/hol-light/Help/INT_NEG_CONV.hlp
/usr/share/hol-light/Help/INT_OF_REAL_THM.hlp
/usr/share/hol-light/Help/INT_POLY_CONV.hlp
/usr/share/hol-light/Help/INT_POW_CONV.hlp
/usr/share/hol-light/Help/INT_REDUCE_CONV.hlp
/usr/share/hol-light/Help/INT_RED_CONV.hlp
/usr/share/hol-light/Help/INT_REM_DOWN_CONV.hlp
/usr/share/hol-light/Help/INT_RING.hlp
/usr/share/hol-light/Help/INT_SGN_CONV.hlp
/usr/share/hol-light/Help/INT_SUB_CONV.hlp
/usr/share/hol-light/Help/ISPEC.hlp
/usr/share/hol-light/Help/ISPECL.hlp
/usr/share/hol-light/Help/ITAUT.hlp
/usr/share/hol-light/Help/ITAUT_TAC.hlp
/usr/share/hol-light/Help/K.hlp
/usr/share/hol-light/Help/LABEL_TAC.hlp
/usr/share/hol-light/Help/LAMBDA_ELIM_CONV.hlp
/usr/share/hol-light/Help/LAND_CONV.hlp
/usr/share/hol-light/Help/LEANCOP.hlp
/usr/share/hol-light/Help/LEANCOP_TAC.hlp
/usr/share/hol-light/Help/LET_TAC.hlp
/usr/share/hol-light/Help/LE_IMP.hlp
/usr/share/hol-light/Help/LIST_CONV.hlp
/usr/share/hol-light/Help/LIST_INDUCT_TAC.hlp
/usr/share/hol-light/Help/MAP_EVERY.hlp
/usr/share/hol-light/Help/MAP_FIRST.hlp
/usr/share/hol-light/Help/MATCH_ACCEPT_TAC.hlp
/usr/share/hol-light/Help/MATCH_CONV.hlp
/usr/share/hol-light/Help/MATCH_MP.hlp
/usr/share/hol-light/Help/MATCH_MP_TAC.hlp
/usr/share/hol-light/Help/MESON.hlp
/usr/share/hol-light/Help/MESON_TAC.hlp
/usr/share/hol-light/Help/META_EXISTS_TAC.hlp
/usr/share/hol-light/Help/META_SPEC_TAC.hlp
/usr/share/hol-light/Help/METIS.hlp
/usr/share/hol-light/Help/METIS_TAC.hlp
/usr/share/hol-light/Help/MK_BINOP_UPPERCASE.hlp
/usr/share/hol-light/Help/MK_COMB_TAC.hlp
/usr/share/hol-light/Help/MK_COMB_UPPERCASE.hlp
/usr/share/hol-light/Help/MK_CONJ_UPPERCASE.hlp
/usr/share/hol-light/Help/MK_DISJ_UPPERCASE.hlp
/usr/share/hol-light/Help/MK_EXISTS_UPPERCASE.hlp
/usr/share/hol-light/Help/MK_FORALL_UPPERCASE.hlp
/usr/share/hol-light/Help/MOD_DOWN_CONV.hlp
/usr/share/hol-light/Help/MONO_TAC.hlp
/usr/share/hol-light/Help/MP.hlp
/usr/share/hol-light/Help/MP_CONV.hlp
/usr/share/hol-light/Help/MP_TAC.hlp
/usr/share/hol-light/Help/NAME_ASSUMS_TAC.hlp
/usr/share/hol-light/Help/NANOCOP.hlp
/usr/share/hol-light/Help/NANOCOP_TAC.hlp
/usr/share/hol-light/Help/NNFC_CONV.hlp
/usr/share/hol-light/Help/NNF_CONV.hlp
/usr/share/hol-light/Help/NOT_ELIM.hlp
/usr/share/hol-light/Help/NOT_INTRO.hlp
/usr/share/hol-light/Help/NO_CONV.hlp
/usr/share/hol-light/Help/NO_TAC.hlp
/usr/share/hol-light/Help/NO_THEN.hlp
/usr/share/hol-light/Help/NUMBER_RULE.hlp
/usr/share/hol-light/Help/NUMBER_TAC.hlp
/usr/share/hol-light/Help/NUMSEG_CONV.hlp
/usr/share/hol-light/Help/NUM_ADD_CONV.hlp
/usr/share/hol-light/Help/NUM_CANCEL_CONV.hlp
/usr/share/hol-light/Help/NUM_DIV_CONV.hlp
/usr/share/hol-light/Help/NUM_EQ_CONV.hlp
/usr/share/hol-light/Help/NUM_EVEN_CONV.hlp
/usr/share/hol-light/Help/NUM_EXP_CONV.hlp
/usr/share/hol-light/Help/NUM_FACT_CONV.hlp
/usr/share/hol-light/Help/NUM_GE_CONV.hlp
/usr/share/hol-light/Help/NUM_GT_CONV.hlp
/usr/share/hol-light/Help/NUM_LE_CONV.hlp
/usr/share/hol-light/Help/NUM_LT_CONV.hlp
/usr/share/hol-light/Help/NUM_MAX_CONV.hlp
/usr/share/hol-light/Help/NUM_MIN_CONV.hlp
/usr/share/hol-light/Help/NUM_MOD_CONV.hlp
/usr/share/hol-light/Help/NUM_MULT_CONV.hlp
/usr/share/hol-light/Help/NUM_NORMALIZE_CONV.hlp
/usr/share/hol-light/Help/NUM_ODD_CONV.hlp
/usr/share/hol-light/Help/NUM_PRE_CONV.hlp
/usr/share/hol-light/Help/NUM_REDUCE_CONV.hlp
/usr/share/hol-light/Help/NUM_REDUCE_TAC.hlp
/usr/share/hol-light/Help/NUM_RED_CONV.hlp
/usr/share/hol-light/Help/NUM_REL_CONV.hlp
/usr/share/hol-light/Help/NUM_RING.hlp
/usr/share/hol-light/Help/NUM_SIMPLIFY_CONV.hlp
/usr/share/hol-light/Help/NUM_SUB_CONV.hlp
/usr/share/hol-light/Help/NUM_SUC_CONV.hlp
/usr/share/hol-light/Help/NUM_TO_INT_CONV.hlp
/usr/share/hol-light/Help/ONCE_ASM_REWRITE_RULE.hlp
/usr/share/hol-light/Help/ONCE_ASM_REWRITE_TAC.hlp
/usr/share/hol-light/Help/ONCE_ASM_SIMP_TAC.hlp
/usr/share/hol-light/Help/ONCE_DEPTH_CONV.hlp
/usr/share/hol-light/Help/ONCE_DEPTH_SQCONV.hlp
/usr/share/hol-light/Help/ONCE_REWRITE_CONV.hlp
/usr/share/hol-light/Help/ONCE_REWRITE_RULE.hlp
/usr/share/hol-light/Help/ONCE_REWRITE_TAC.hlp
/usr/share/hol-light/Help/ONCE_SIMPLIFY_CONV.hlp
/usr/share/hol-light/Help/ONCE_SIMP_CONV.hlp
/usr/share/hol-light/Help/ONCE_SIMP_RULE.hlp
/usr/share/hol-light/Help/ONCE_SIMP_TAC.hlp
/usr/share/hol-light/Help/ORDERED_IMP_REWR_CONV.hlp
/usr/share/hol-light/Help/ORDERED_REWR_CONV.hlp
/usr/share/hol-light/Help/ORELSE.hlp
/usr/share/hol-light/Help/ORELSEC.hlp
/usr/share/hol-light/Help/ORELSE_TCL.hlp
/usr/share/hol-light/Help/PART_MATCH.hlp
/usr/share/hol-light/Help/PATH_CONV.hlp
/usr/share/hol-light/Help/PAT_CONV.hlp
/usr/share/hol-light/Help/PINST.hlp
/usr/share/hol-light/Help/POP_ASSUM.hlp
/usr/share/hol-light/Help/POP_ASSUM_LIST.hlp
/usr/share/hol-light/Help/PRENEX_CONV.hlp
/usr/share/hol-light/Help/PRESIMP_CONV.hlp
/usr/share/hol-light/Help/PRINT_GOAL_TAC.hlp
/usr/share/hol-light/Help/PROP_ATOM_CONV.hlp
/usr/share/hol-light/Help/PROVE_HYP.hlp
/usr/share/hol-light/Help/PURE_ASM_REWRITE_RULE.hlp
/usr/share/hol-light/Help/PURE_ASM_REWRITE_TAC.hlp
/usr/share/hol-light/Help/PURE_ASM_SIMP_TAC.hlp
/usr/share/hol-light/Help/PURE_ONCE_ASM_REWRITE_RULE.hlp
/usr/share/hol-light/Help/PURE_ONCE_ASM_REWRITE_TAC.hlp
/usr/share/hol-light/Help/PURE_ONCE_REWRITE_CONV.hlp
/usr/share/hol-light/Help/PURE_ONCE_REWRITE_RULE.hlp
/usr/share/hol-light/Help/PURE_ONCE_REWRITE_TAC.hlp
/usr/share/hol-light/Help/PURE_REWRITE_CONV.hlp
/usr/share/hol-light/Help/PURE_REWRITE_RULE.hlp
/usr/share/hol-light/Help/PURE_REWRITE_TAC.hlp
/usr/share/hol-light/Help/PURE_SIMP_CONV.hlp
/usr/share/hol-light/Help/PURE_SIMP_RULE.hlp
/usr/share/hol-light/Help/PURE_SIMP_TAC.hlp
/usr/share/hol-light/Help/RAND_CONV.hlp
/usr/share/hol-light/Help/RATOR_CONV.hlp
/usr/share/hol-light/Help/REAL_ARITH.hlp
/usr/share/hol-light/Help/REAL_ARITH_TAC.hlp
/usr/share/hol-light/Help/REAL_FIELD.hlp
/usr/share/hol-light/Help/REAL_IDEAL_CONV.hlp
/usr/share/hol-light/Help/REAL_INT_ABS_CONV.hlp
/usr/share/hol-light/Help/REAL_INT_ADD_CONV.hlp
/usr/share/hol-light/Help/REAL_INT_EQ_CONV.hlp
/usr/share/hol-light/Help/REAL_INT_GE_CONV.hlp
/usr/share/hol-light/Help/REAL_INT_GT_CONV.hlp
/usr/share/hol-light/Help/REAL_INT_LE_CONV.hlp
/usr/share/hol-light/Help/REAL_INT_LT_CONV.hlp
/usr/share/hol-light/Help/REAL_INT_MUL_CONV.hlp
/usr/share/hol-light/Help/REAL_INT_NEG_CONV.hlp
/usr/share/hol-light/Help/REAL_INT_POW_CONV.hlp
/usr/share/hol-light/Help/REAL_INT_RAT_CONV.hlp
/usr/share/hol-light/Help/REAL_INT_REDUCE_CONV.hlp
/usr/share/hol-light/Help/REAL_INT_RED_CONV.hlp
/usr/share/hol-light/Help/REAL_INT_SUB_CONV.hlp
/usr/share/hol-light/Help/REAL_LET_IMP.hlp
/usr/share/hol-light/Help/REAL_LE_IMP.hlp
/usr/share/hol-light/Help/REAL_LINEAR_PROVER.hlp
/usr/share/hol-light/Help/REAL_POLY_ADD_CONV.hlp
/usr/share/hol-light/Help/REAL_POLY_CONV.hlp
/usr/share/hol-light/Help/REAL_POLY_MUL_CONV.hlp
/usr/share/hol-light/Help/REAL_POLY_NEG_CONV.hlp
/usr/share/hol-light/Help/REAL_POLY_POW_CONV.hlp
/usr/share/hol-light/Help/REAL_POLY_SUB_CONV.hlp
/usr/share/hol-light/Help/REAL_RAT_ABS_CONV.hlp
/usr/share/hol-light/Help/REAL_RAT_ADD_CONV.hlp
/usr/share/hol-light/Help/REAL_RAT_DIV_CONV.hlp
/usr/share/hol-light/Help/REAL_RAT_EQ_CONV.hlp
/usr/share/hol-light/Help/REAL_RAT_GE_CONV.hlp
/usr/share/hol-light/Help/REAL_RAT_GT_CONV.hlp
/usr/share/hol-light/Help/REAL_RAT_INV_CONV.hlp
/usr/share/hol-light/Help/REAL_RAT_LE_CONV.hlp
/usr/share/hol-light/Help/REAL_RAT_LT_CONV.hlp
/usr/share/hol-light/Help/REAL_RAT_MAX_CONV.hlp
/usr/share/hol-light/Help/REAL_RAT_MIN_CONV.hlp
/usr/share/hol-light/Help/REAL_RAT_MUL_CONV.hlp
/usr/share/hol-light/Help/REAL_RAT_NEG_CONV.hlp
/usr/share/hol-light/Help/REAL_RAT_POW_CONV.hlp
/usr/share/hol-light/Help/REAL_RAT_REDUCE_CONV.hlp
/usr/share/hol-light/Help/REAL_RAT_RED_CONV.hlp
/usr/share/hol-light/Help/REAL_RAT_SGN_CONV.hlp
/usr/share/hol-light/Help/REAL_RAT_SUB_CONV.hlp
/usr/share/hol-light/Help/REAL_RING.hlp
/usr/share/hol-light/Help/RECALL_ACCEPT_TAC.hlp
/usr/share/hol-light/Help/REDEPTH_CONV.hlp
/usr/share/hol-light/Help/REDEPTH_SQCONV.hlp
/usr/share/hol-light/Help/REFL.hlp
/usr/share/hol-light/Help/REFL_TAC.hlp
/usr/share/hol-light/Help/REFUTE_THEN.hlp
/usr/share/hol-light/Help/REMOVE_THEN.hlp
/usr/share/hol-light/Help/REPEATC.hlp
/usr/share/hol-light/Help/REPEAT_GTCL.hlp
/usr/share/hol-light/Help/REPEAT_TCL.hlp
/usr/share/hol-light/Help/REPEAT_UPPERCASE.hlp
/usr/share/hol-light/Help/REPLICATE_TAC.hlp
/usr/share/hol-light/Help/REWRITES_CONV.hlp
/usr/share/hol-light/Help/REWRITE_CONV.hlp
/usr/share/hol-light/Help/REWRITE_RULE.hlp
/usr/share/hol-light/Help/REWRITE_TAC.hlp
/usr/share/hol-light/Help/REWR_CONV.hlp
/usr/share/hol-light/Help/RIGHT_BETAS.hlp
/usr/share/hol-light/Help/RING.hlp
/usr/share/hol-light/Help/RING_AND_IDEAL_CONV.hlp
/usr/share/hol-light/Help/RULE_ASSUM_TAC.hlp
/usr/share/hol-light/Help/SELECT_CONV.hlp
/usr/share/hol-light/Help/SELECT_ELIM_TAC.hlp
/usr/share/hol-light/Help/SELECT_RULE.hlp
/usr/share/hol-light/Help/SEMIRING_NORMALIZERS_CONV.hlp
/usr/share/hol-light/Help/SEQ_IMP_REWRITE_TAC.hlp
/usr/share/hol-light/Help/SET_RULE.hlp
/usr/share/hol-light/Help/SET_TAC.hlp
/usr/share/hol-light/Help/SIMPLE_CHOOSE.hlp
/usr/share/hol-light/Help/SIMPLE_DISJ_CASES.hlp
/usr/share/hol-light/Help/SIMPLE_EXISTS.hlp
/usr/share/hol-light/Help/SIMPLIFY_CONV.hlp
/usr/share/hol-light/Help/SIMP_CONV.hlp
/usr/share/hol-light/Help/SIMP_RULE.hlp
/usr/share/hol-light/Help/SIMP_TAC.hlp
/usr/share/hol-light/Help/SKOLEM_CONV.hlp
/usr/share/hol-light/Help/SPEC.hlp
/usr/share/hol-light/Help/SPECL.hlp
/usr/share/hol-light/Help/SPEC_ALL.hlp
/usr/share/hol-light/Help/SPEC_TAC.hlp
/usr/share/hol-light/Help/SPEC_VAR.hlp
/usr/share/hol-light/Help/STRING_EQ_CONV.hlp
/usr/share/hol-light/Help/STRIP_ASSUME_TAC.hlp
/usr/share/hol-light/Help/STRIP_GOAL_THEN.hlp
/usr/share/hol-light/Help/STRIP_TAC.hlp
/usr/share/hol-light/Help/STRIP_THM_THEN.hlp
/usr/share/hol-light/Help/STRUCT_CASES_TAC.hlp
/usr/share/hol-light/Help/STRUCT_CASES_THEN.hlp
/usr/share/hol-light/Help/SUBGOAL_TAC.hlp
/usr/share/hol-light/Help/SUBGOAL_THEN.hlp
/usr/share/hol-light/Help/SUBLET_CONV.hlp
/usr/share/hol-light/Help/SUBS.hlp
/usr/share/hol-light/Help/SUBST1_TAC.hlp
/usr/share/hol-light/Help/SUBST_ALL_TAC.hlp
/usr/share/hol-light/Help/SUBST_VAR_TAC.hlp
/usr/share/hol-light/Help/SUBS_CONV.hlp
/usr/share/hol-light/Help/SUB_CONV.hlp
/usr/share/hol-light/Help/SYM.hlp
/usr/share/hol-light/Help/SYM_CONV.hlp
/usr/share/hol-light/Help/TAC_PROOF.hlp
/usr/share/hol-light/Help/TARGET_REWRITE_TAC.hlp
/usr/share/hol-light/Help/TAUT.hlp
/usr/share/hol-light/Help/THEN.hlp
/usr/share/hol-light/Help/THENC.hlp
/usr/share/hol-light/Help/THENL.hlp
/usr/share/hol-light/Help/THEN_TCL.hlp
/usr/share/hol-light/Help/TOP_DEPTH_CONV.hlp
/usr/share/hol-light/Help/TOP_DEPTH_SQCONV.hlp
/usr/share/hol-light/Help/TOP_SWEEP_CONV.hlp
/usr/share/hol-light/Help/TOP_SWEEP_SQCONV.hlp
/usr/share/hol-light/Help/TRANS.hlp
/usr/share/hol-light/Help/TRANS_TAC.hlp
/usr/share/hol-light/Help/TRY.hlp
/usr/share/hol-light/Help/TRY_CONV.hlp
/usr/share/hol-light/Help/UNDISCH.hlp
/usr/share/hol-light/Help/UNDISCH_ALL.hlp
/usr/share/hol-light/Help/UNDISCH_TAC.hlp
/usr/share/hol-light/Help/UNDISCH_THEN.hlp
/usr/share/hol-light/Help/UNIFY_ACCEPT_TAC.hlp
/usr/share/hol-light/Help/UNWIND_CONV.hlp
/usr/share/hol-light/Help/USE_THEN.hlp
/usr/share/hol-light/Help/VALID.hlp
/usr/share/hol-light/Help/W.hlp
/usr/share/hol-light/Help/WEAK_CNF_CONV.hlp
/usr/share/hol-light/Help/WEAK_DNF_CONV.hlp
/usr/share/hol-light/Help/WF_INDUCT_TAC.hlp
/usr/share/hol-light/Help/X_CHOOSE_TAC.hlp
/usr/share/hol-light/Help/X_CHOOSE_THEN.hlp
/usr/share/hol-light/Help/X_GEN_TAC.hlp
/usr/share/hol-light/Help/X_META_EXISTS_TAC.hlp
/usr/share/hol-light/Help/a.hlp
/usr/share/hol-light/Help/aconv.hlp
/usr/share/hol-light/Help/allpairs.hlp
/usr/share/hol-light/Help/alpha.hlp
/usr/share/hol-light/Help/alphaorder.hlp
/usr/share/hol-light/Help/apply.hlp
/usr/share/hol-light/Help/apply_prover.hlp
/usr/share/hol-light/Help/applyd.hlp
/usr/share/hol-light/Help/assoc.hlp
/usr/share/hol-light/Help/assocd.hlp
/usr/share/hol-light/Help/atleast.hlp
/usr/share/hol-light/Help/atoms.hlp
/usr/share/hol-light/Help/aty.hlp
/usr/share/hol-light/Help/augment.hlp
/usr/share/hol-light/Help/axioms.hlp
/usr/share/hol-light/Help/b.hlp
/usr/share/hol-light/Help/basic_congs.hlp
/usr/share/hol-light/Help/basic_convs.hlp
/usr/share/hol-light/Help/basic_net.hlp
/usr/share/hol-light/Help/basic_prover.hlp
/usr/share/hol-light/Help/basic_rectype_net.hlp
/usr/share/hol-light/Help/basic_rewrites.hlp
/usr/share/hol-light/Help/basic_ss.hlp
/usr/share/hol-light/Help/binders.hlp
/usr/share/hol-light/Help/binops.hlp
/usr/share/hol-light/Help/bndvar.hlp
/usr/share/hol-light/Help/body.hlp
/usr/share/hol-light/Help/bool_ty.hlp
/usr/share/hol-light/Help/bty.hlp
/usr/share/hol-light/Help/butlast.hlp
/usr/share/hol-light/Help/by.hlp
/usr/share/hol-light/Help/can.hlp
/usr/share/hol-light/Help/cases.hlp
/usr/share/hol-light/Help/check.hlp
/usr/share/hol-light/Help/checkpoint.hlp
/usr/share/hol-light/Help/choose.hlp
/usr/share/hol-light/Help/chop_list.hlp
/usr/share/hol-light/Help/combine.hlp
/usr/share/hol-light/Help/comment_token.hlp
/usr/share/hol-light/Help/compose_insts.hlp
/usr/share/hol-light/Help/concl.hlp
/usr/share/hol-light/Help/conjuncts.hlp
/usr/share/hol-light/Help/constants.hlp
/usr/share/hol-light/Help/copverb.hlp
/usr/share/hol-light/Help/current_goalstack.hlp
/usr/share/hol-light/Help/curry.hlp
/usr/share/hol-light/Help/decreasing.hlp
/usr/share/hol-light/Help/deep_alpha.hlp
/usr/share/hol-light/Help/define.hlp
/usr/share/hol-light/Help/define_quotient_type.hlp
/usr/share/hol-light/Help/define_type.hlp
/usr/share/hol-light/Help/define_type_raw.hlp
/usr/share/hol-light/Help/defined.hlp
/usr/share/hol-light/Help/definitions.hlp
/usr/share/hol-light/Help/delete_parser.hlp
/usr/share/hol-light/Help/delete_user_printer.hlp
/usr/share/hol-light/Help/denominator.hlp
/usr/share/hol-light/Help/derive_nonschematic_inductive_relations.hlp
/usr/share/hol-light/Help/derive_strong_induction.hlp
/usr/share/hol-light/Help/dest_abs.hlp
/usr/share/hol-light/Help/dest_binary.hlp
/usr/share/hol-light/Help/dest_binder.hlp
/usr/share/hol-light/Help/dest_binop.hlp
/usr/share/hol-light/Help/dest_char.hlp
/usr/share/hol-light/Help/dest_comb.hlp
/usr/share/hol-light/Help/dest_cond.hlp
/usr/share/hol-light/Help/dest_conj.hlp
/usr/share/hol-light/Help/dest_cons.hlp
/usr/share/hol-light/Help/dest_const.hlp
/usr/share/hol-light/Help/dest_disj.hlp
/usr/share/hol-light/Help/dest_eq.hlp
/usr/share/hol-light/Help/dest_exists.hlp
/usr/share/hol-light/Help/dest_finty.hlp
/usr/share/hol-light/Help/dest_forall.hlp
/usr/share/hol-light/Help/dest_fun_ty.hlp
/usr/share/hol-light/Help/dest_gabs.hlp
/usr/share/hol-light/Help/dest_iff.hlp
/usr/share/hol-light/Help/dest_imp.hlp
/usr/share/hol-light/Help/dest_intconst.hlp
/usr/share/hol-light/Help/dest_let.hlp
/usr/share/hol-light/Help/dest_list.hlp
/usr/share/hol-light/Help/dest_neg.hlp
/usr/share/hol-light/Help/dest_numeral.hlp
/usr/share/hol-light/Help/dest_pair.hlp
/usr/share/hol-light/Help/dest_realintconst.hlp
/usr/share/hol-light/Help/dest_select.hlp
/usr/share/hol-light/Help/dest_setenum.hlp
/usr/share/hol-light/Help/dest_small_numeral.hlp
/usr/share/hol-light/Help/dest_string.hlp
/usr/share/hol-light/Help/dest_thm.hlp
/usr/share/hol-light/Help/dest_type.hlp
/usr/share/hol-light/Help/dest_uexists.hlp
/usr/share/hol-light/Help/dest_var.hlp
/usr/share/hol-light/Help/dest_vartype.hlp
/usr/share/hol-light/Help/disjuncts.hlp
/usr/share/hol-light/Help/distinctness.hlp
/usr/share/hol-light/Help/distinctness_store.hlp
/usr/share/hol-light/Help/do_list.hlp
/usr/share/hol-light/Help/dom.hlp
/usr/share/hol-light/Help/dpty.hlp
/usr/share/hol-light/Help/e.hlp
/usr/share/hol-light/Help/el.hlp
/usr/share/hol-light/Help/elistof.hlp
/usr/share/hol-light/Help/empty_net.hlp
/usr/share/hol-light/Help/empty_ss.hlp
/usr/share/hol-light/Help/end_itlist.hlp
/usr/share/hol-light/Help/enter.hlp
/usr/share/hol-light/Help/equals_goal.hlp
/usr/share/hol-light/Help/equals_thm.hlp
/usr/share/hol-light/Help/exactly.hlp
/usr/share/hol-light/Help/exists.hlp
/usr/share/hol-light/Help/explode.hlp
/usr/share/hol-light/Help/extend_basic_congs.hlp
/usr/share/hol-light/Help/extend_basic_convs.hlp
/usr/share/hol-light/Help/extend_basic_rewrites.hlp
/usr/share/hol-light/Help/extend_rectype_net.hlp
/usr/share/hol-light/Help/f_f_.hlp
/usr/share/hol-light/Help/fail.hlp
/usr/share/hol-light/Help/file_of_string.hlp
/usr/share/hol-light/Help/file_on_path.hlp
/usr/share/hol-light/Help/filter.hlp
/usr/share/hol-light/Help/find.hlp
/usr/share/hol-light/Help/find_path.hlp
/usr/share/hol-light/Help/find_term.hlp
/usr/share/hol-light/Help/find_terms.hlp
/usr/share/hol-light/Help/finished.hlp
/usr/share/hol-light/Help/fix.hlp
/usr/share/hol-light/Help/flat.hlp
/usr/share/hol-light/Help/flush_goalstack.hlp
/usr/share/hol-light/Help/foldl.hlp
/usr/share/hol-light/Help/foldr.hlp
/usr/share/hol-light/Help/follow_path.hlp
/usr/share/hol-light/Help/forall.hlp
/usr/share/hol-light/Help/forall2.hlp
/usr/share/hol-light/Help/free_in.hlp
/usr/share/hol-light/Help/frees.hlp
/usr/share/hol-light/Help/freesin.hlp
/usr/share/hol-light/Help/freesl.hlp
/usr/share/hol-light/Help/funpow.hlp
/usr/share/hol-light/Help/g.hlp
/usr/share/hol-light/Help/gcd.hlp
/usr/share/hol-light/Help/gcd_num.hlp
/usr/share/hol-light/Help/genvar.hlp
/usr/share/hol-light/Help/get_const_type.hlp
/usr/share/hol-light/Help/get_infix_status.hlp
/usr/share/hol-light/Help/get_type_arity.hlp
/usr/share/hol-light/Help/graph.hlp
/usr/share/hol-light/Help/hd.hlp
/usr/share/hol-light/Help/help.hlp
/usr/share/hol-light/Help/help_path.hlp
/usr/share/hol-light/Help/hide_constant.hlp
/usr/share/hol-light/Help/hol_dir.hlp
/usr/share/hol-light/Help/hol_expand_directory.hlp
/usr/share/hol-light/Help/hol_version.hlp
/usr/share/hol-light/Help/hyp.hlp
/usr/share/hol-light/Help/ideal_cofactors.hlp
/usr/share/hol-light/Help/ignore_constant_varstruct.hlp
/usr/share/hol-light/Help/implode.hlp
/usr/share/hol-light/Help/increasing.hlp
/usr/share/hol-light/Help/index.hlp
/usr/share/hol-light/Help/inductive_type_store.hlp
/usr/share/hol-light/Help/infixes.hlp
/usr/share/hol-light/Help/injectivity.hlp
/usr/share/hol-light/Help/injectivity_store.hlp
/usr/share/hol-light/Help/insert.hlp
/usr/share/hol-light/Help/insert_prime.hlp
/usr/share/hol-light/Help/inst.hlp
/usr/share/hol-light/Help/inst_goal.hlp
/usr/share/hol-light/Help/install_parser.hlp
/usr/share/hol-light/Help/install_user_printer.hlp
/usr/share/hol-light/Help/installed_parsers.hlp
/usr/share/hol-light/Help/instantiate.hlp
/usr/share/hol-light/Help/instantiate_casewise_recursion.hlp
/usr/share/hol-light/Help/int_ideal_cofactors.hlp
/usr/share/hol-light/Help/intersect.hlp
/usr/share/hol-light/Help/is_abs.hlp
/usr/share/hol-light/Help/is_binary.hlp
/usr/share/hol-light/Help/is_binder.hlp
/usr/share/hol-light/Help/is_binop.hlp
/usr/share/hol-light/Help/is_comb.hlp
/usr/share/hol-light/Help/is_cond.hlp
/usr/share/hol-light/Help/is_conj.hlp
/usr/share/hol-light/Help/is_cons.hlp
/usr/share/hol-light/Help/is_const.hlp
/usr/share/hol-light/Help/is_disj.hlp
/usr/share/hol-light/Help/is_eq.hlp
/usr/share/hol-light/Help/is_exists.hlp
/usr/share/hol-light/Help/is_forall.hlp
/usr/share/hol-light/Help/is_gabs.hlp
/usr/share/hol-light/Help/is_hidden.hlp
/usr/share/hol-light/Help/is_iff.hlp
/usr/share/hol-light/Help/is_imp.hlp
/usr/share/hol-light/Help/is_intconst.hlp
/usr/share/hol-light/Help/is_let.hlp
/usr/share/hol-light/Help/is_list.hlp
/usr/share/hol-light/Help/is_neg.hlp
/usr/share/hol-light/Help/is_numeral.hlp
/usr/share/hol-light/Help/is_pair.hlp
/usr/share/hol-light/Help/is_prefix.hlp
/usr/share/hol-light/Help/is_ratconst.hlp
/usr/share/hol-light/Help/is_realintconst.hlp
/usr/share/hol-light/Help/is_reserved_word.hlp
/usr/share/hol-light/Help/is_select.hlp
/usr/share/hol-light/Help/is_setenum.hlp
/usr/share/hol-light/Help/is_type.hlp
/usr/share/hol-light/Help/is_uexists.hlp
/usr/share/hol-light/Help/is_undefined.hlp
/usr/share/hol-light/Help/is_var.hlp
/usr/share/hol-light/Help/is_vartype.hlp
/usr/share/hol-light/Help/isalnum.hlp
/usr/share/hol-light/Help/isalpha.hlp
/usr/share/hol-light/Help/isbra.hlp
/usr/share/hol-light/Help/isnum.hlp
/usr/share/hol-light/Help/issep.hlp
/usr/share/hol-light/Help/isspace.hlp
/usr/share/hol-light/Help/issymb.hlp
/usr/share/hol-light/Help/it.hlp
/usr/share/hol-light/Help/itlist.hlp
/usr/share/hol-light/Help/itlist2.hlp
/usr/share/hol-light/Help/last.hlp
/usr/share/hol-light/Help/lcm_num.hlp
/usr/share/hol-light/Help/leftbin.hlp
/usr/share/hol-light/Help/length.hlp
/usr/share/hol-light/Help/let_CONV.hlp
/usr/share/hol-light/Help/lex.hlp
/usr/share/hol-light/Help/lhand.hlp
/usr/share/hol-light/Help/lhs.hlp
/usr/share/hol-light/Help/lift_function.hlp
/usr/share/hol-light/Help/lift_theorem.hlp
/usr/share/hol-light/Help/list_mk_abs.hlp
/usr/share/hol-light/Help/list_mk_binop.hlp
/usr/share/hol-light/Help/list_mk_comb.hlp
/usr/share/hol-light/Help/list_mk_conj.hlp
/usr/share/hol-light/Help/list_mk_disj.hlp
/usr/share/hol-light/Help/list_mk_exists.hlp
/usr/share/hol-light/Help/list_mk_forall.hlp
/usr/share/hol-light/Help/list_mk_gabs.hlp
/usr/share/hol-light/Help/list_mk_icomb.hlp
/usr/share/hol-light/Help/listof.hlp
/usr/share/hol-light/Help/load_on_path.hlp
/usr/share/hol-light/Help/load_path.hlp
/usr/share/hol-light/Help/loaded_files.hlp
/usr/share/hol-light/Help/loads.hlp
/usr/share/hol-light/Help/loadt.hlp
/usr/share/hol-light/Help/lookup.hlp
/usr/share/hol-light/Help/make_args.hlp
/usr/share/hol-light/Help/make_overloadable.hlp
/usr/share/hol-light/Help/many.hlp
/usr/share/hol-light/Help/map.hlp
/usr/share/hol-light/Help/map2.hlp
/usr/share/hol-light/Help/mapf.hlp
/usr/share/hol-light/Help/mapfilter.hlp
/usr/share/hol-light/Help/mem.hlp
/usr/share/hol-light/Help/mem_prime.hlp
/usr/share/hol-light/Help/merge.hlp
/usr/share/hol-light/Help/merge_nets.hlp
/usr/share/hol-light/Help/mergesort.hlp
/usr/share/hol-light/Help/meson_brand.hlp
/usr/share/hol-light/Help/meson_chatty.hlp
/usr/share/hol-light/Help/meson_dcutin.hlp
/usr/share/hol-light/Help/meson_depth.hlp
/usr/share/hol-light/Help/meson_prefine.hlp
/usr/share/hol-light/Help/meson_skew.hlp
/usr/share/hol-light/Help/meson_split_limit.hlp
/usr/share/hol-light/Help/metisverb.hlp
/usr/share/hol-light/Help/mk_abs.hlp
/usr/share/hol-light/Help/mk_binary.hlp
/usr/share/hol-light/Help/mk_binder.hlp
/usr/share/hol-light/Help/mk_binop.hlp
/usr/share/hol-light/Help/mk_char.hlp
/usr/share/hol-light/Help/mk_comb.hlp
/usr/share/hol-light/Help/mk_cond.hlp
/usr/share/hol-light/Help/mk_conj.hlp
/usr/share/hol-light/Help/mk_cons.hlp
/usr/share/hol-light/Help/mk_const.hlp
/usr/share/hol-light/Help/mk_disj.hlp
/usr/share/hol-light/Help/mk_eq.hlp
/usr/share/hol-light/Help/mk_exists.hlp
/usr/share/hol-light/Help/mk_finty.hlp
/usr/share/hol-light/Help/mk_flist.hlp
/usr/share/hol-light/Help/mk_forall.hlp
/usr/share/hol-light/Help/mk_fset.hlp
/usr/share/hol-light/Help/mk_fthm.hlp
/usr/share/hol-light/Help/mk_fun_ty.hlp
/usr/share/hol-light/Help/mk_gabs.hlp
/usr/share/hol-light/Help/mk_goalstate.hlp
/usr/share/hol-light/Help/mk_icomb.hlp
/usr/share/hol-light/Help/mk_iff.hlp
/usr/share/hol-light/Help/mk_imp.hlp
/usr/share/hol-light/Help/mk_intconst.hlp
/usr/share/hol-light/Help/mk_let.hlp
/usr/share/hol-light/Help/mk_list.hlp
/usr/share/hol-light/Help/mk_mconst.hlp
/usr/share/hol-light/Help/mk_neg.hlp
/usr/share/hol-light/Help/mk_numeral.hlp
/usr/share/hol-light/Help/mk_pair.hlp
/usr/share/hol-light/Help/mk_primed_var.hlp
/usr/share/hol-light/Help/mk_prover.hlp
/usr/share/hol-light/Help/mk_realintconst.hlp
/usr/share/hol-light/Help/mk_rewrites.hlp
/usr/share/hol-light/Help/mk_select.hlp
/usr/share/hol-light/Help/mk_setenum.hlp
/usr/share/hol-light/Help/mk_small_numeral.hlp
/usr/share/hol-light/Help/mk_string.hlp
/usr/share/hol-light/Help/mk_thm.hlp
/usr/share/hol-light/Help/mk_type.hlp
/usr/share/hol-light/Help/mk_uexists.hlp
/usr/share/hol-light/Help/mk_var.hlp
/usr/share/hol-light/Help/mk_vartype.hlp
/usr/share/hol-light/Help/monotonicity_theorems.hlp
/usr/share/hol-light/Help/name.hlp
/usr/share/hol-light/Help/name_of.hlp
/usr/share/hol-light/Help/needs.hlp
/usr/share/hol-light/Help/net_of_cong.hlp
/usr/share/hol-light/Help/net_of_conv.hlp
/usr/share/hol-light/Help/net_of_thm.hlp
/usr/share/hol-light/Help/new_axiom.hlp
/usr/share/hol-light/Help/new_basic_definition.hlp
/usr/share/hol-light/Help/new_basic_type_definition.hlp
/usr/share/hol-light/Help/new_constant.hlp
/usr/share/hol-light/Help/new_definition.hlp
/usr/share/hol-light/Help/new_inductive_definition.hlp
/usr/share/hol-light/Help/new_inductive_set.hlp
/usr/share/hol-light/Help/new_recursive_definition.hlp
/usr/share/hol-light/Help/new_specification.hlp
/usr/share/hol-light/Help/new_type.hlp
/usr/share/hol-light/Help/new_type_abbrev.hlp
/usr/share/hol-light/Help/new_type_definition.hlp
/usr/share/hol-light/Help/nothing.hlp
/usr/share/hol-light/Help/nsplit.hlp
/usr/share/hol-light/Help/null_inst.hlp
/usr/share/hol-light/Help/null_meta.hlp
/usr/share/hol-light/Help/num_0.hlp
/usr/share/hol-light/Help/num_1.hlp
/usr/share/hol-light/Help/num_10.hlp
/usr/share/hol-light/Help/num_2.hlp
/usr/share/hol-light/Help/num_CONV.hlp
/usr/share/hol-light/Help/num_of_string.hlp
/usr/share/hol-light/Help/numdom.hlp
/usr/share/hol-light/Help/numerator.hlp
/usr/share/hol-light/Help/o.hlp
/usr/share/hol-light/Help/occurs_in.hlp
/usr/share/hol-light/Help/omit.hlp
/usr/share/hol-light/Help/orelse_.hlp
/usr/share/hol-light/Help/orelse_tcl_.hlp
/usr/share/hol-light/Help/orelsec_.hlp
/usr/share/hol-light/Help/overload_interface.hlp
/usr/share/hol-light/Help/override_interface.hlp
/usr/share/hol-light/Help/p.hlp
/usr/share/hol-light/Help/parse_as_binder.hlp
/usr/share/hol-light/Help/parse_as_infix.hlp
/usr/share/hol-light/Help/parse_as_prefix.hlp
/usr/share/hol-light/Help/parse_inductive_type_specification.hlp
/usr/share/hol-light/Help/parse_preterm.hlp
/usr/share/hol-light/Help/parse_pretype.hlp
/usr/share/hol-light/Help/parse_term.hlp
/usr/share/hol-light/Help/parse_type.hlp
/usr/share/hol-light/Help/parses_as_binder.hlp
/usr/share/hol-light/Help/partition.hlp
/usr/share/hol-light/Help/possibly.hlp
/usr/share/hol-light/Help/pow10.hlp
/usr/share/hol-light/Help/pow2.hlp
/usr/share/hol-light/Help/pp_print_fpf.hlp
/usr/share/hol-light/Help/pp_print_num.hlp
/usr/share/hol-light/Help/pp_print_qterm.hlp
/usr/share/hol-light/Help/pp_print_qtype.hlp
/usr/share/hol-light/Help/pp_print_term.hlp
/usr/share/hol-light/Help/pp_print_thm.hlp
/usr/share/hol-light/Help/pp_print_type.hlp
/usr/share/hol-light/Help/prebroken_binops.hlp
/usr/share/hol-light/Help/prefixes.hlp
/usr/share/hol-light/Help/preterm_of_term.hlp
/usr/share/hol-light/Help/pretype_of_type.hlp
/usr/share/hol-light/Help/print_all_thm.hlp
/usr/share/hol-light/Help/print_fpf.hlp
/usr/share/hol-light/Help/print_goal.hlp
/usr/share/hol-light/Help/print_goal_hyp_max_boxes.hlp
/usr/share/hol-light/Help/print_goalstack.hlp
/usr/share/hol-light/Help/print_num.hlp
/usr/share/hol-light/Help/print_qterm.hlp
/usr/share/hol-light/Help/print_qtype.hlp
/usr/share/hol-light/Help/print_term.hlp
/usr/share/hol-light/Help/print_thm.hlp
/usr/share/hol-light/Help/print_to_string.hlp
/usr/share/hol-light/Help/print_type.hlp
/usr/share/hol-light/Help/print_types_of_subterms.hlp
/usr/share/hol-light/Help/print_unambiguous_comprehensions.hlp
/usr/share/hol-light/Help/prioritize_int.hlp
/usr/share/hol-light/Help/prioritize_num.hlp
/usr/share/hol-light/Help/prioritize_overload.hlp
/usr/share/hol-light/Help/prioritize_real.hlp
/usr/share/hol-light/Help/prove.hlp
/usr/share/hol-light/Help/prove_cases_thm.hlp
/usr/share/hol-light/Help/prove_constructors_distinct.hlp
/usr/share/hol-light/Help/prove_constructors_injective.hlp
/usr/share/hol-light/Help/prove_general_recursive_function_exists.hlp
/usr/share/hol-light/Help/prove_inductive_relations_exist.hlp
/usr/share/hol-light/Help/prove_monotonicity_hyps.hlp
/usr/share/hol-light/Help/prove_recursive_functions_exist.hlp
/usr/share/hol-light/Help/pure_prove_recursive_function_exists.hlp
/usr/share/hol-light/Help/qmap.hlp
/usr/share/hol-light/Help/quotexpander.hlp
/usr/share/hol-light/Help/r.hlp
/usr/share/hol-light/Help/ran.hlp
/usr/share/hol-light/Help/rand.hlp
/usr/share/hol-light/Help/rat_of_term.hlp
/usr/share/hol-light/Help/rator.hlp
/usr/share/hol-light/Help/real_ideal_cofactors.hlp
/usr/share/hol-light/Help/reduce_interface.hlp
/usr/share/hol-light/Help/refine.hlp
/usr/share/hol-light/Help/remark.hlp
/usr/share/hol-light/Help/remove.hlp
/usr/share/hol-light/Help/remove_interface.hlp
/usr/share/hol-light/Help/remove_type_abbrev.hlp
/usr/share/hol-light/Help/repeat.hlp
/usr/share/hol-light/Help/replicate.hlp
/usr/share/hol-light/Help/report.hlp
/usr/share/hol-light/Help/report_timing.hlp
/usr/share/hol-light/Help/reserve_words.hlp
/usr/share/hol-light/Help/reserved_words.hlp
/usr/share/hol-light/Help/retypecheck.hlp
/usr/share/hol-light/Help/rev.hlp
/usr/share/hol-light/Help/rev_assoc.hlp
/usr/share/hol-light/Help/rev_assocd.hlp
/usr/share/hol-light/Help/rev_itlist.hlp
/usr/share/hol-light/Help/rev_itlist2.hlp
/usr/share/hol-light/Help/rev_splitlist.hlp
/usr/share/hol-light/Help/reverse_interface_mapping.hlp
/usr/share/hol-light/Help/rhs.hlp
/usr/share/hol-light/Help/rightbin.hlp
/usr/share/hol-light/Help/rotate.hlp
/usr/share/hol-light/Help/search.hlp
/usr/share/hol-light/Help/self_destruct.hlp
/usr/share/hol-light/Help/set_basic_congs.hlp
/usr/share/hol-light/Help/set_basic_convs.hlp
/usr/share/hol-light/Help/set_basic_rewrites.hlp
/usr/share/hol-light/Help/set_eq.hlp
/usr/share/hol-light/Help/set_goal.hlp
/usr/share/hol-light/Help/set_verbose_symbols.hlp
/usr/share/hol-light/Help/setify.hlp
/usr/share/hol-light/Help/shareout.hlp
/usr/share/hol-light/Help/some.hlp
/usr/share/hol-light/Help/sort.hlp
/usr/share/hol-light/Help/splitlist.hlp
/usr/share/hol-light/Help/ss_of_congs.hlp
/usr/share/hol-light/Help/ss_of_conv.hlp
/usr/share/hol-light/Help/ss_of_maker.hlp
/usr/share/hol-light/Help/ss_of_prover.hlp
/usr/share/hol-light/Help/ss_of_provers.hlp
/usr/share/hol-light/Help/ss_of_thms.hlp
/usr/share/hol-light/Help/startup_banner.hlp
/usr/share/hol-light/Help/string_of_file.hlp
/usr/share/hol-light/Help/string_of_term.hlp
/usr/share/hol-light/Help/string_of_thm.hlp
/usr/share/hol-light/Help/string_of_type.hlp
/usr/share/hol-light/Help/strings_of_file.hlp
/usr/share/hol-light/Help/strip_abs.hlp
/usr/share/hol-light/Help/strip_comb.hlp
/usr/share/hol-light/Help/strip_exists.hlp
/usr/share/hol-light/Help/strip_forall.hlp
/usr/share/hol-light/Help/strip_gabs.hlp
/usr/share/hol-light/Help/strip_ncomb.hlp
/usr/share/hol-light/Help/striplist.hlp
/usr/share/hol-light/Help/subset.hlp
/usr/share/hol-light/Help/subst.hlp
/usr/share/hol-light/Help/subtract.hlp
/usr/share/hol-light/Help/subtract_prime.hlp
/usr/share/hol-light/Help/temp_path.hlp
/usr/share/hol-light/Help/term_match.hlp
/usr/share/hol-light/Help/term_of_preterm.hlp
/usr/share/hol-light/Help/term_of_rat.hlp
/usr/share/hol-light/Help/term_order.hlp
/usr/share/hol-light/Help/term_type_unify.hlp
/usr/share/hol-light/Help/term_unify.hlp
/usr/share/hol-light/Help/term_union.hlp
/usr/share/hol-light/Help/the_definitions.hlp
/usr/share/hol-light/Help/the_implicit_types.hlp
/usr/share/hol-light/Help/the_inductive_definitions.hlp
/usr/share/hol-light/Help/the_inductive_types.hlp
/usr/share/hol-light/Help/the_interface.hlp
/usr/share/hol-light/Help/the_overload_skeletons.hlp
/usr/share/hol-light/Help/the_specifications.hlp
/usr/share/hol-light/Help/the_type_definitions.hlp
/usr/share/hol-light/Help/then_.hlp
/usr/share/hol-light/Help/then_tcl_.hlp
/usr/share/hol-light/Help/thenc_.hlp
/usr/share/hol-light/Help/thenl_.hlp
/usr/share/hol-light/Help/theorems.hlp
/usr/share/hol-light/Help/thm_frees.hlp
/usr/share/hol-light/Help/time.hlp
/usr/share/hol-light/Help/tl.hlp
/usr/share/hol-light/Help/top_goal.hlp
/usr/share/hol-light/Help/top_realgoal.hlp
/usr/share/hol-light/Help/top_thm.hlp
/usr/share/hol-light/Help/try_user_parser.hlp
/usr/share/hol-light/Help/try_user_printer.hlp
/usr/share/hol-light/Help/tryapplyd.hlp
/usr/share/hol-light/Help/tryfind.hlp
/usr/share/hol-light/Help/type_abbrevs.hlp
/usr/share/hol-light/Help/type_invention_error.hlp
/usr/share/hol-light/Help/type_invention_warning.hlp
/usr/share/hol-light/Help/type_match.hlp
/usr/share/hol-light/Help/type_of.hlp
/usr/share/hol-light/Help/type_of_pretype.hlp
/usr/share/hol-light/Help/type_subst.hlp
/usr/share/hol-light/Help/type_unify.hlp
/usr/share/hol-light/Help/type_vars_in_term.hlp
/usr/share/hol-light/Help/types.hlp
/usr/share/hol-light/Help/typify_universal_set.hlp
/usr/share/hol-light/Help/tysubst.hlp
/usr/share/hol-light/Help/tyvars.hlp
/usr/share/hol-light/Help/uncurry.hlp
/usr/share/hol-light/Help/undefine.hlp
/usr/share/hol-light/Help/undefined.hlp
/usr/share/hol-light/Help/unhide_constant.hlp
/usr/share/hol-light/Help/union.hlp
/usr/share/hol-light/Help/union_prime.hlp
/usr/share/hol-light/Help/unions.hlp
/usr/share/hol-light/Help/unions_prime.hlp
/usr/share/hol-light/Help/uniq.hlp
/usr/share/hol-light/Help/unparse_as_binder.hlp
/usr/share/hol-light/Help/unparse_as_infix.hlp
/usr/share/hol-light/Help/unparse_as_prefix.hlp
/usr/share/hol-light/Help/unreserve_words.hlp
/usr/share/hol-light/Help/unset_jrh_lexer.hlp
/usr/share/hol-light/Help/unset_then_multiple_subgoals.hlp
/usr/share/hol-light/Help/unset_verbose_symbols.hlp
/usr/share/hol-light/Help/unspaced_binops.hlp
/usr/share/hol-light/Help/unzip.hlp
/usr/share/hol-light/Help/use_file.hlp
/usr/share/hol-light/Help/use_file_raise_failure.hlp
/usr/share/hol-light/Help/variables.hlp
/usr/share/hol-light/Help/variant.hlp
/usr/share/hol-light/Help/variants.hlp
/usr/share/hol-light/Help/verbose.hlp
/usr/share/hol-light/Help/vfree_in.hlp
/usr/share/hol-light/Help/vsubst.hlp
/usr/share/hol-light/Help/warn.hlp
/usr/share/hol-light/Help/zip.hlp
/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/bdd.ml
/usr/share/hol-light/Library/binary.ml
/usr/share/hol-light/Library/binomial.ml
/usr/share/hol-light/Library/bitmatch.ml
/usr/share/hol-light/Library/bitsize.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/frag.ml
/usr/share/hol-light/Library/grouptheory.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/jacobi.ml
/usr/share/hol-light/Library/modmul_group.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/ringtheory.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/Library/words.ml
/usr/share/hol-light/Logic/README
/usr/share/hol-light/Logic/birkhoff.ml
/usr/share/hol-light/Logic/canon.ml
/usr/share/hol-light/Logic/fol.ml
/usr/share/hol-light/Logic/fol_prop.ml
/usr/share/hol-light/Logic/fole.ml
/usr/share/hol-light/Logic/given.ml
/usr/share/hol-light/Logic/givensem.ml
/usr/share/hol-light/Logic/herbrand.ml
/usr/share/hol-light/Logic/linear.ml
/usr/share/hol-light/Logic/lpo.ml
/usr/share/hol-light/Logic/make.ml
/usr/share/hol-light/Logic/positive.ml
/usr/share/hol-light/Logic/prenex.ml
/usr/share/hol-light/Logic/prolog.ml
/usr/share/hol-light/Logic/resolution.ml
/usr/share/hol-light/Logic/skolem.ml
/usr/share/hol-light/Logic/support.ml
/usr/share/hol-light/Logic/trs.ml
/usr/share/hol-light/Logic/unif.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/test.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/homology.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/msum.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/specialtopologies.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/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/ProofTrace/.gitignore
/usr/share/hol-light/ProofTrace/README
/usr/share/hol-light/ProofTrace/fusion.ml.diff
/usr/share/hol-light/ProofTrace/proofs.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/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/src/DetectEq.java
/usr/share/hol-light/Proofrecording/tools/src/Makefile
/usr/share/hol-light/Proofrecording/tools/src/NamedTheorem.java
/usr/share/hol-light/Proofrecording/tools/startcore.ml
/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/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/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/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/arith.ml
/usr/share/hol-light/basics.ml
/usr/share/hol-light/bignum.cmi
/usr/share/hol-light/bignum.cmo
/usr/share/hol-light/bignum_num.ml
/usr/share/hol-light/bignum_zarith.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/compute.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/firstorder.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/hol.sh
/usr/share/hol-light/hol_4.14.sh
/usr/share/hol-light/hol_4.sh
/usr/share/hol-light/hol_lib.ml
/usr/share/hol-light/hol_lib_use_module.ml
/usr/share/hol-light/hol_loader.cmi
/usr/share/hol-light/hol_loader.cmo
/usr/share/hol-light/hol_loader.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/inline_load.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/load_camlp4.ml
/usr/share/hol-light/load_camlp5.ml
/usr/share/hol-light/load_camlp5_topfind.ml
/usr/share/hol-light/make.ml
/usr/share/hol-light/meson.ml
/usr/share/hol-light/metis.ml
/usr/share/hol-light/miz3/ERRORS
/usr/share/hol-light/miz3/README
/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/exrc
/usr/share/hol-light/miz3/grammar/miz3.y
/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/nets.ml
/usr/share/hol-light/normalizer.ml
/usr/share/hol-light/nums.ml
/usr/share/hol-light/ocaml-hol
/usr/share/hol-light/ocamlinit-stamp
/usr/share/hol-light/pa_j.cmi
/usr/share/hol-light/pa_j.cmo
/usr/share/hol-light/pa_j/README
/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/thecops.ml
/usr/share/hol-light/theorems.ml
/usr/share/hol-light/trivia.ml
/usr/share/hol-light/unit_tests.ml
/usr/share/hol-light/update_database.ml
/usr/share/hol-light/update_database/update_database_3.ml
/usr/share/hol-light/update_database/update_database_4.14.ml
/usr/share/hol-light/update_database/update_database_4.ml
/usr/share/hol-light/update_database/update_database_5.ml
/usr/share/hol-light/wf.ml
/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