Stéphane Glondu pushed to branch upstream at Debian OCaml Maintainers / hol-light
Commits:
-
1a8c714e
by Stephane Glondu at 2025-12-20T03:39:27+01:00
90 changed files:
- .github/workflows/main.yml
- .gitignore
- + 100/transcendence.ml
- CHANGES
- Examples/bitblast.ml
- + Examples/bitblast_generic.ml
- Help/ASM.hlp
- + Help/EL_CONV.hlp
- + Help/LENGTH_CONV.hlp
- Help/LIST_CONV.hlp
- + Help/LIST_OF_SEQ_CONV.hlp
- Help/PRINT_GOAL_TAC.hlp
- + Help/PRINT_TERM_CONV.hlp
- + Help/REMARK_TAC.hlp
- + Help/REVERSE_CONV.hlp
- Help/b.hlp
- + Help/delete_user_color_printer.hlp
- Help/delete_user_printer.hlp
- Help/e.hlp
- + Help/er.hlp
- + Help/find_index.hlp
- Help/g.hlp
- Help/index.hlp
- + Help/install_user_color_printer.hlp
- Help/install_user_printer.hlp
- Help/load_path.hlp
- Help/loadt.hlp
- Help/p.hlp
- + Help/pp_print_colored_qterm.hlp
- + Help/pp_print_colored_qtype.hlp
- + Help/pp_print_colored_term.hlp
- + Help/pp_print_colored_thm.hlp
- + Help/pp_print_colored_type.hlp
- Help/pp_print_qterm.hlp
- Help/pp_print_qtype.hlp
- Help/pp_print_term.hlp
- Help/pp_print_thm.hlp
- Help/pp_print_type.hlp
- Help/r.hlp
- Help/remark.hlp
- + Help/set_color_printer.hlp
- − Help/term_union.hlp
- + Help/try_user_color_printer.hlp
- Help/try_user_printer.hlp
- Help/unset_then_multiple_subgoals.hlp
- Library/bdd.ml
- Library/binomial.ml
- Library/bitmatch.ml
- + Library/fieldtheory.ml
- + Library/matroids.ml
- Library/primitive.ml
- Library/ringtheory.ml
- + Library/word_automata.ml
- Library/words.ml
- + META
- Makefile
- Multivariate/complex_database.ml
- Multivariate/make.ml
- Multivariate/make_complex.ml
- Multivariate/multivariate_database.ml
- Multivariate/vectors.ml
- ProofTrace/README
- ProofTrace/fusion.ml.diff
- README
- bignum_zarith.ml
- calc_int.ml
- calc_num.ml
- calc_rat.ml
- compute.ml
- database.ml
- define.ml
- equal.ml
- hol.ml
- hol_4.14.sh
- hol_4.sh
- hol_lib.ml
- hol_loader.ml
- holtest
- holtest.mk
- ind_defs.ml
- int.ml
- lib.ml
- lists.ml
- + make-checkpoint.sh
- − make.ml
- + opam
- printer.ml
- sets.ml
- tactics.ml
- unit_tests.ml