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