hol88-library-source (2.02.19940316dfsg-9)
2 versions available in kali/kali-last-snapshot/main/i386
Details
Core information at a glance
- Distribution
- kali
- Origin
- kali-last-snapshot
- Repository
- https://http.kali.org/kali
- Codename
- kali-last-snapshot
- Component
- main
- Source
- hol88
- Architecture
- i386
- Section
- math
- Priority
- optional
- Maintainer
- Camm Maguire <[email protected]>
Size & integrity
Byte sizes and integrity verification
- Installed size
- 3.5 kB
- Size expected
- 410.5 kB
- Size actual
- 410.5 kB
- Size match
Dependencies
Required package dependencies
- None
Suggested packages
Recommended additional packages
- None
Description
Higher Order Logic, library source files
Tags
Package classification tags
role::source
Checksums
Hash values and integrity verification status
| Type | Actual | Match |
|---|---|---|
| MD5 | 7bf610d9…ffc1cfd4 | |
| SHA-1 | 2162b901…f156968d | |
| SHA-256 | 8221fc97…4b86301a | |
| SHA-512 | a92ddd17…448e5ded |
Contents
Files and directories included
. usr usr/share usr/share/doc usr/share/doc/hol88-library-source usr/share/doc/hol88-library-source/changelog.Debian.gz usr/share/doc/hol88-library-source/copyright usr/share/hol88-2.02.19940316dfsg usr/share/hol88-2.02.19940316dfsg/Library usr/share/hol88-2.02.19940316dfsg/Library/abs_theory usr/share/hol88-2.02.19940316dfsg/Library/abs_theory/abs_theory.ml usr/share/hol88-2.02.19940316dfsg/Library/abs_theory/example.ml usr/share/hol88-2.02.19940316dfsg/Library/abs_theory/group_def.ml usr/share/hol88-2.02.19940316dfsg/Library/abs_theory/monoid_def.ml usr/share/hol88-2.02.19940316dfsg/Library/arith usr/share/hol88-2.02.19940316dfsg/Library/arith/arith.ml usr/share/hol88-2.02.19940316dfsg/Library/arith/arith_cons.ml usr/share/hol88-2.02.19940316dfsg/Library/arith/decls.ml usr/share/hol88-2.02.19940316dfsg/Library/arith/exists_arith.ml usr/share/hol88-2.02.19940316dfsg/Library/arith/gen_arith.ml usr/share/hol88-2.02.19940316dfsg/Library/arith/instance.ml usr/share/hol88-2.02.19940316dfsg/Library/arith/int_extra.ml usr/share/hol88-2.02.19940316dfsg/Library/arith/norm_arith.ml usr/share/hol88-2.02.19940316dfsg/Library/arith/norm_bool.ml usr/share/hol88-2.02.19940316dfsg/Library/arith/norm_ineqs.ml usr/share/hol88-2.02.19940316dfsg/Library/arith/prenex.ml usr/share/hol88-2.02.19940316dfsg/Library/arith/qconv.ml usr/share/hol88-2.02.19940316dfsg/Library/arith/rationals.ml usr/share/hol88-2.02.19940316dfsg/Library/arith/sol_ranges.ml usr/share/hol88-2.02.19940316dfsg/Library/arith/solve.ml usr/share/hol88-2.02.19940316dfsg/Library/arith/solve_ineqs.ml usr/share/hol88-2.02.19940316dfsg/Library/arith/streams.ml usr/share/hol88-2.02.19940316dfsg/Library/arith/string_extra.ml usr/share/hol88-2.02.19940316dfsg/Library/arith/sub_and_cond.ml usr/share/hol88-2.02.19940316dfsg/Library/arith/sup-inf.ml usr/share/hol88-2.02.19940316dfsg/Library/arith/term_coeffs.ml usr/share/hol88-2.02.19940316dfsg/Library/arith/theorems.ml usr/share/hol88-2.02.19940316dfsg/Library/arith/thm_convs.ml usr/share/hol88-2.02.19940316dfsg/Library/finite_sets usr/share/hol88-2.02.19940316dfsg/Library/finite_sets/OLD usr/share/hol88-2.02.19940316dfsg/Library/finite_sets/OLD/card.ml usr/share/hol88-2.02.19940316dfsg/Library/finite_sets/OLD/finite_sets.ml usr/share/hol88-2.02.19940316dfsg/Library/finite_sets/OLD/load_finite_sets.ml usr/share/hol88-2.02.19940316dfsg/Library/finite_sets/OLD/mk_finite_sets.ml usr/share/hol88-2.02.19940316dfsg/Library/finite_sets/OLD/set_ind.ml usr/share/hol88-2.02.19940316dfsg/Library/finite_sets/finite_sets.ml usr/share/hol88-2.02.19940316dfsg/Library/finite_sets/fset_conv.ml usr/share/hol88-2.02.19940316dfsg/Library/finite_sets/load_finite_sets.ml usr/share/hol88-2.02.19940316dfsg/Library/finite_sets/mk_finite_sets.ml usr/share/hol88-2.02.19940316dfsg/Library/finite_sets/set_ind.ml usr/share/hol88-2.02.19940316dfsg/Library/ind_defs usr/share/hol88-2.02.19940316dfsg/Library/ind_defs/Examples usr/share/hol88-2.02.19940316dfsg/Library/ind_defs/Examples/exp.ml usr/share/hol88-2.02.19940316dfsg/Library/ind_defs/Examples/rtc.ml usr/share/hol88-2.02.19940316dfsg/Library/ind_defs/ind-defs.ml usr/share/hol88-2.02.19940316dfsg/Library/ind_defs/ind_defs.ml usr/share/hol88-2.02.19940316dfsg/Library/latex-hol usr/share/hol88-2.02.19940316dfsg/Library/latex-hol/filters.ml usr/share/hol88-2.02.19940316dfsg/Library/latex-hol/formaters.ml usr/share/hol88-2.02.19940316dfsg/Library/latex-hol/hol_trees.ml usr/share/hol88-2.02.19940316dfsg/Library/latex-hol/latex-hol.ml usr/share/hol88-2.02.19940316dfsg/Library/latex-hol/precedence.ml usr/share/hol88-2.02.19940316dfsg/Library/more_arithmetic usr/share/hol88-2.02.19940316dfsg/Library/more_arithmetic/add.ml usr/share/hol88-2.02.19940316dfsg/Library/more_arithmetic/bool_convs.ml usr/share/hol88-2.02.19940316dfsg/Library/more_arithmetic/div_mod.ml usr/share/hol88-2.02.19940316dfsg/Library/more_arithmetic/ineq.ml usr/share/hol88-2.02.19940316dfsg/Library/more_arithmetic/load_more_arithmetic.ml usr/share/hol88-2.02.19940316dfsg/Library/more_arithmetic/minmax.ml usr/share/hol88-2.02.19940316dfsg/Library/more_arithmetic/mk_more_arithmetic.ml usr/share/hol88-2.02.19940316dfsg/Library/more_arithmetic/more_arithmetic.ml usr/share/hol88-2.02.19940316dfsg/Library/more_arithmetic/mult.ml usr/share/hol88-2.02.19940316dfsg/Library/more_arithmetic/normalize.ml usr/share/hol88-2.02.19940316dfsg/Library/more_arithmetic/num_convs.ml usr/share/hol88-2.02.19940316dfsg/Library/more_arithmetic/num_tac.ml usr/share/hol88-2.02.19940316dfsg/Library/more_arithmetic/odd_even.ml usr/share/hol88-2.02.19940316dfsg/Library/more_arithmetic/pre.ml usr/share/hol88-2.02.19940316dfsg/Library/more_arithmetic/sub.ml usr/share/hol88-2.02.19940316dfsg/Library/more_arithmetic/suc.ml usr/share/hol88-2.02.19940316dfsg/Library/more_arithmetic/tools.ml usr/share/hol88-2.02.19940316dfsg/Library/more_arithmetic/zero.ml usr/share/hol88-2.02.19940316dfsg/Library/numeral usr/share/hol88-2.02.19940316dfsg/Library/numeral/define.ml usr/share/hol88-2.02.19940316dfsg/Library/numeral/numeral.ml usr/share/hol88-2.02.19940316dfsg/Library/numeral/numeral_rules.ml usr/share/hol88-2.02.19940316dfsg/Library/numeral/numeral_theory.ml usr/share/hol88-2.02.19940316dfsg/Library/numeral/sanity_test.ml usr/share/hol88-2.02.19940316dfsg/Library/pair usr/share/hol88-2.02.19940316dfsg/Library/pair/all.ml usr/share/hol88-2.02.19940316dfsg/Library/pair/basic.ml usr/share/hol88-2.02.19940316dfsg/Library/pair/both1.ml usr/share/hol88-2.02.19940316dfsg/Library/pair/both2.ml usr/share/hol88-2.02.19940316dfsg/Library/pair/conv.ml usr/share/hol88-2.02.19940316dfsg/Library/pair/exi.ml usr/share/hol88-2.02.19940316dfsg/Library/pair/pair.ml usr/share/hol88-2.02.19940316dfsg/Library/pair/syn.ml usr/share/hol88-2.02.19940316dfsg/Library/parser usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/HOL usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/HOL/loader.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/HOL/term.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/HOL/term_decls.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/HOL/term_help.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/HOL/type.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/HOL/type_decls.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/A1_1.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/A1_10.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/A1_10_decls.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/A1_11.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/A1_11_decls.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/A1_1_decls.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/A1_2.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/A1_2_decls.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/A1_3.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/A1_3_decls.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/A1_4.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/A1_4_decls.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/A1_5.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/A1_5_decls.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/A1_6.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/A1_6_decls.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/A1_7.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/A1_7_decls.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/A1_8.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/A1_8_decls.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/A1_9.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/A1_9_decls.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/PP_command.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/PP_printer.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/full-ella.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/general.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/loader.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/v1_help.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/ella/version0_PP.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/tiny usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/tiny/examples.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/tiny/loader.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/tiny/tiny.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/tiny/tiny_decls.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/tiny/tiny_help.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/user_guide usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/user_guide/blocks usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/user_guide/blocks/blocks.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/user_guide/blocks/blocks_decls.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/user_guide/blocks/loader.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/user_guide/bool usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/user_guide/bool/bool.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/user_guide/bool/bool_decls.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/user_guide/bool/loader.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/user_guide/types usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/user_guide/types/loader.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/user_guide/types/types.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/user_guide/types/types_decls.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/Examples/user_guide/types/types_help.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/general.ml usr/share/hol88-2.02.19940316dfsg/Library/parser/parser.ml usr/share/hol88-2.02.19940316dfsg/Library/pred_sets usr/share/hol88-2.02.19940316dfsg/Library/pred_sets/OLD usr/share/hol88-2.02.19940316dfsg/Library/pred_sets/OLD/load_pred_sets.ml usr/share/hol88-2.02.19940316dfsg/Library/pred_sets/OLD/mk_pred_set_defs.ml usr/share/hol88-2.02.19940316dfsg/Library/pred_sets/OLD/mk_pred_sets.ml usr/share/hol88-2.02.19940316dfsg/Library/pred_sets/OLD/pred_sets.ml usr/share/hol88-2.02.19940316dfsg/Library/pred_sets/fset_conv.ml usr/share/hol88-2.02.19940316dfsg/Library/pred_sets/gspec.ml usr/share/hol88-2.02.19940316dfsg/Library/pred_sets/load_pred_sets.ml usr/share/hol88-2.02.19940316dfsg/Library/pred_sets/mk_pred_sets.ml usr/share/hol88-2.02.19940316dfsg/Library/pred_sets/pred_sets.ml usr/share/hol88-2.02.19940316dfsg/Library/pred_sets/set_ind.ml usr/share/hol88-2.02.19940316dfsg/Library/prettyp usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_hol usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_hol/PP_hol.ml usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_hol/hol_trees.ml usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_hol/link_to_hol.ml usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_hol/new_printers.ml usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_hol/precedence.ml usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_hol.ml usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_parser usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_parser/PP_parser.ml usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_parser/PP_to_ML.ml usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_parser/convert.ml usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_parser/generate.ml usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_parser/lex.ml usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_parser/syntax.ml usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_parser.ml usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_printer usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_printer/PP_printer.ml usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_printer/boxes.ml usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_printer/boxtostring.ml usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_printer/extents.ml usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_printer/print.ml usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_printer/ptree.ml usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_printer/strings.ml usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_printer/treematch.ml usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_printer/treetobox.ml usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_printer/utils.ml usr/share/hol88-2.02.19940316dfsg/Library/prettyp/PP_printer.ml usr/share/hol88-2.02.19940316dfsg/Library/prettyp/prettyp.ml usr/share/hol88-2.02.19940316dfsg/Library/reals usr/share/hol88-2.02.19940316dfsg/Library/reals/load_reals.ml usr/share/hol88-2.02.19940316dfsg/Library/reals/reals.ml usr/share/hol88-2.02.19940316dfsg/Library/reals/theories usr/share/hol88-2.02.19940316dfsg/Library/reals/theories/autoload_reals.ml usr/share/hol88-2.02.19940316dfsg/Library/reals/theories/equiv.ml usr/share/hol88-2.02.19940316dfsg/Library/reals/theories/hrat.ml usr/share/hol88-2.02.19940316dfsg/Library/reals/theories/hreal.ml usr/share/hol88-2.02.19940316dfsg/Library/reals/theories/lim.ml usr/share/hol88-2.02.19940316dfsg/Library/reals/theories/nets.ml usr/share/hol88-2.02.19940316dfsg/Library/reals/theories/powser.ml usr/share/hol88-2.02.19940316dfsg/Library/reals/theories/real.ml usr/share/hol88-2.02.19940316dfsg/Library/reals/theories/realax.ml usr/share/hol88-2.02.19940316dfsg/Library/reals/theories/seq.ml usr/share/hol88-2.02.19940316dfsg/Library/reals/theories/topology.ml usr/share/hol88-2.02.19940316dfsg/Library/reals/theories/transc.ml usr/share/hol88-2.02.19940316dfsg/Library/reals/theories/useful.ml usr/share/hol88-2.02.19940316dfsg/Library/record_proof usr/share/hol88-2.02.19940316dfsg/Library/record_proof/benchmark usr/share/hol88-2.02.19940316dfsg/Library/record_proof/benchmark/HOL_MULT.ml usr/share/hol88-2.02.19940316dfsg/Library/record_proof/benchmark/MULT_FUN.ml usr/share/hol88-2.02.19940316dfsg/Library/record_proof/benchmark/MULT_FUN_CURRY.ml usr/share/hol88-2.02.19940316dfsg/Library/record_proof/benchmark/mk_NEXT.ml usr/share/hol88-2.02.19940316dfsg/Library/record_proof/benchmark/unwind.ml usr/share/hol88-2.02.19940316dfsg/Library/record_proof/disable.ml usr/share/hol88-2.02.19940316dfsg/Library/record_proof/dummy_funs.ml usr/share/hol88-2.02.19940316dfsg/Library/record_proof/enable.ml usr/share/hol88-2.02.19940316dfsg/Library/record_proof/proof_rec.ml usr/share/hol88-2.02.19940316dfsg/Library/record_proof/record_proof.ml usr/share/hol88-2.02.19940316dfsg/Library/reduce usr/share/hol88-2.02.19940316dfsg/Library/reduce/arithconv.ml usr/share/hol88-2.02.19940316dfsg/Library/reduce/boolconv.ml usr/share/hol88-2.02.19940316dfsg/Library/reduce/reduce.ml usr/share/hol88-2.02.19940316dfsg/Library/res_quan usr/share/hol88-2.02.19940316dfsg/Library/res_quan/cond_rewr.ml usr/share/hol88-2.02.19940316dfsg/Library/res_quan/cond_rewrite.ml usr/share/hol88-2.02.19940316dfsg/Library/res_quan/help usr/share/hol88-2.02.19940316dfsg/Library/res_quan/help/entries usr/share/hol88-2.02.19940316dfsg/Library/res_quan/help/entries/hol-init.ml usr/share/hol88-2.02.19940316dfsg/Library/res_quan/load_res_quan.ml usr/share/hol88-2.02.19940316dfsg/Library/res_quan/mk_res_quan.ml usr/share/hol88-2.02.19940316dfsg/Library/res_quan/res_quan.ml usr/share/hol88-2.02.19940316dfsg/Library/res_quan/res_rules.ml usr/share/hol88-2.02.19940316dfsg/Library/sets usr/share/hol88-2.02.19940316dfsg/Library/sets/fset_conv.ml usr/share/hol88-2.02.19940316dfsg/Library/sets/gspec.ml usr/share/hol88-2.02.19940316dfsg/Library/sets/load_sets.ml usr/share/hol88-2.02.19940316dfsg/Library/sets/mk_sets.ml usr/share/hol88-2.02.19940316dfsg/Library/sets/set_ind.ml usr/share/hol88-2.02.19940316dfsg/Library/sets/sets.ml usr/share/hol88-2.02.19940316dfsg/Library/string usr/share/hol88-2.02.19940316dfsg/Library/string/ascii.ml usr/share/hol88-2.02.19940316dfsg/Library/string/load_string.ml usr/share/hol88-2.02.19940316dfsg/Library/string/mk_ascii.ml usr/share/hol88-2.02.19940316dfsg/Library/string/mk_string.ml usr/share/hol88-2.02.19940316dfsg/Library/string/string.ml usr/share/hol88-2.02.19940316dfsg/Library/string/string_rules.ml usr/share/hol88-2.02.19940316dfsg/Library/string/stringconv.ml usr/share/hol88-2.02.19940316dfsg/Library/taut usr/share/hol88-2.02.19940316dfsg/Library/taut/taut.ml usr/share/hol88-2.02.19940316dfsg/Library/taut/taut_check.ml usr/share/hol88-2.02.19940316dfsg/Library/trs usr/share/hol88-2.02.19940316dfsg/Library/trs/extents.ml usr/share/hol88-2.02.19940316dfsg/Library/trs/extract.ml usr/share/hol88-2.02.19940316dfsg/Library/trs/matching.ml usr/share/hol88-2.02.19940316dfsg/Library/trs/name.ml usr/share/hol88-2.02.19940316dfsg/Library/trs/search.ml usr/share/hol88-2.02.19940316dfsg/Library/trs/sets.ml usr/share/hol88-2.02.19940316dfsg/Library/trs/sidecond.ml usr/share/hol88-2.02.19940316dfsg/Library/trs/struct.ml usr/share/hol88-2.02.19940316dfsg/Library/trs/thmkind.ml usr/share/hol88-2.02.19940316dfsg/Library/trs/trs.ml usr/share/hol88-2.02.19940316dfsg/Library/trs/user.ml usr/share/hol88-2.02.19940316dfsg/Library/unwind usr/share/hol88-2.02.19940316dfsg/Library/unwind/old usr/share/hol88-2.02.19940316dfsg/Library/unwind/old/des-unwind.ml usr/share/hol88-2.02.19940316dfsg/Library/unwind/old/mjcg-unwind.ml usr/share/hol88-2.02.19940316dfsg/Library/unwind/old/unwind.ml usr/share/hol88-2.02.19940316dfsg/Library/unwind/unwind.ml usr/share/hol88-2.02.19940316dfsg/Library/unwind/unwinding.ml usr/share/hol88-2.02.19940316dfsg/Library/wellorder usr/share/hol88-2.02.19940316dfsg/Library/wellorder/load_wellorder.ml usr/share/hol88-2.02.19940316dfsg/Library/wellorder/mk_wellorder.ml usr/share/hol88-2.02.19940316dfsg/Library/wellorder/wellorder.ml usr/share/hol88-2.02.19940316dfsg/Library/window usr/share/hol88-2.02.19940316dfsg/Library/window/basic_close.ml usr/share/hol88-2.02.19940316dfsg/Library/window/eq_close.ml usr/share/hol88-2.02.19940316dfsg/Library/window/help usr/share/hol88-2.02.19940316dfsg/Library/window/help/general usr/share/hol88-2.02.19940316dfsg/Library/window/help/general/signal.ml usr/share/hol88-2.02.19940316dfsg/Library/window/hol_ext.ml usr/share/hol88-2.02.19940316dfsg/Library/window/imp_close.ml usr/share/hol88-2.02.19940316dfsg/Library/window/inter.ml usr/share/hol88-2.02.19940316dfsg/Library/window/load_code.ml usr/share/hol88-2.02.19940316dfsg/Library/window/load_window.ml usr/share/hol88-2.02.19940316dfsg/Library/window/mk_win_th.ml usr/share/hol88-2.02.19940316dfsg/Library/window/ml_ext.ml usr/share/hol88-2.02.19940316dfsg/Library/window/tables.ml usr/share/hol88-2.02.19940316dfsg/Library/window/tactic.ml usr/share/hol88-2.02.19940316dfsg/Library/window/thms.ml usr/share/hol88-2.02.19940316dfsg/Library/window/win.ml usr/share/hol88-2.02.19940316dfsg/Library/window/window.ml usr/share/hol88-2.02.19940316dfsg/Library/window/xlabel.ml usr/share/hol88-2.02.19940316dfsg/Library/word usr/share/hol88-2.02.19940316dfsg/Library/word/arith_thms.ml usr/share/hol88-2.02.19940316dfsg/Library/word/genfuns.ml usr/share/hol88-2.02.19940316dfsg/Library/word/load_parent.ml usr/share/hol88-2.02.19940316dfsg/Library/word/mk_bword_arith.ml usr/share/hol88-2.02.19940316dfsg/Library/word/mk_bword_bitop.ml usr/share/hol88-2.02.19940316dfsg/Library/word/mk_bword_num.ml usr/share/hol88-2.02.19940316dfsg/Library/word/mk_word.ml usr/share/hol88-2.02.19940316dfsg/Library/word/mk_word_arith.ml usr/share/hol88-2.02.19940316dfsg/Library/word/mk_word_base.ml usr/share/hol88-2.02.19940316dfsg/Library/word/mk_word_bitop.ml usr/share/hol88-2.02.19940316dfsg/Library/word/mk_word_num.ml usr/share/hol88-2.02.19940316dfsg/Library/word/ver_202.ml usr/share/hol88-2.02.19940316dfsg/Library/word/word.ml usr/share/hol88-2.02.19940316dfsg/Library/word/word_convs.ml usr/share/hol88-2.02.19940316dfsg/Library/word/word_funs.ml