GitHub - brain-research/hol-light: Patched version of HOL Light with tactic logging for machine learning purposes

This repository was archived by the owner on Apr 19, 2026. It is now read-only.

Name		Name	Last commit message	Last commit date
100		100
Arithmetic		Arithmetic
Boyer_Moore		Boyer_Moore
Complex		Complex
Examples		Examples
Formal_ineqs		Formal_ineqs
Functionspaces		Functionspaces
Help		Help
IEEE		IEEE
IsabelleLight		IsabelleLight
Jordan		Jordan
LP_arith		LP_arith
Library		Library
Minisat		Minisat
Mizarlight		Mizarlight
Model		Model
Multivariate		Multivariate
Ntrie		Ntrie
Permutation		Permutation
QBF		QBF
Quaternions		Quaternions
RichterHilbertAxiomGeometry		RichterHilbertAxiomGeometry
Rqe		Rqe
Tutorial		Tutorial
Unity		Unity
api		api
miz3		miz3
scripts		scripts
tests		tests
.gitignore		.gitignore
CHANGES		CHANGES
Dockerfile		Dockerfile
Dockerfile_check_proofs		Dockerfile_check_proofs
LICENSE		LICENSE
Makefile		Makefile
QUICK_REFERENCE.txt		QUICK_REFERENCE.txt
README		README
VERYQUICK_REFERENCE.txt		VERYQUICK_REFERENCE.txt
arith.ml		arith.ml
basics.ml		basics.ml
bool.ml		bool.ml
calc_int.ml		calc_int.ml
calc_num.ml		calc_num.ml
calc_rat.ml		calc_rat.ml
canon.ml		canon.ml
cart.ml		cart.ml
class.ml		class.ml
comms.ml		comms.ml
comms_wrapper.cc		comms_wrapper.cc
conv_tac_params.rb		conv_tac_params.rb
database.ml		database.ml
debug_mode.ml		debug_mode.ml
define.ml		define.ml
doc-to-help.sed		doc-to-help.sed
drule.ml		drule.ml
equal.ml		equal.ml
farmhash_compatibility.h		farmhash_compatibility.h
file_list.rb		file_list.rb
finish.ml		finish.ml
fusion.ml		fusion.ml
grobner.ml		grobner.ml
help.ml		help.ml
hol.ml		hol.ml
hol_native.ml		hol_native.ml
holtest		holtest
holtest.mk		holtest.mk
holtest_parallel		holtest_parallel
impconv.ml		impconv.ml
import_proofs.ml		import_proofs.ml
import_proofs_summary.ml		import_proofs_summary.ml
ind_defs.ml		ind_defs.ml
ind_types.ml		ind_types.ml
ints.ml		ints.ml
itab.ml		itab.ml
iterate.ml		iterate.ml
lib.ml		lib.ml
lists.ml		lists.ml
log.ml		log.ml
make.ml		make.ml
match_paren.rb		match_paren.rb
match_paren_rewrite.rb		match_paren_rewrite.rb
match_quotes.rb		match_quotes.rb
meson.ml		meson.ml
metis.ml		metis.ml
native		native
native-rewrite		native-rewrite
nets.ml		nets.ml
normalize.ml		normalize.ml
normalizer.ml		normalizer.ml
nums.ml		nums.ml
pa_j_3.07.ml		pa_j_3.07.ml
pa_j_3.08.ml		pa_j_3.08.ml
pa_j_3.09.ml		pa_j_3.09.ml
pa_j_3.1x_5.xx.ml		pa_j_3.1x_5.xx.ml
pa_j_3.1x_6.02.1.ml		pa_j_3.1x_6.02.1.ml
pa_j_3.1x_6.02.2.ml		pa_j_3.1x_6.02.2.ml
pa_j_3.1x_6.11.ml		pa_j_3.1x_6.11.ml
pa_j_3.1x_6.xx.ml		pa_j_3.1x_6.xx.ml
pa_j_tweak.ml		pa_j_tweak.ml
pair.ml		pair.ml

Repository files navigation

This repository contains an implementation of the HOList proof assistant API
based on HOL Light (https://www.cl.cam.ac.uk/~jrh13/hol-light/).

For more information about HOList, see http://deephol.org.