Files

 master

/

100

/

Copy path

Directory actions

More options

Directory actions

More options

Latest commit

jrh13

Changed the behaviour of the basic "prove" construct for performing

Aug 1, 2022

8822aa4 · Aug 1, 2022

History

History

This branch is 36 commits ahead of, 138 commits behind jrh13/hol-light:master.

/

100

/

Top

Folders and files

Name		Name	Last commit message	Last commit date
parent directory ..
arithmetic.ml		arithmetic.ml	Removed trailing whitespace in many files	Oct 6, 2021
arithmetic_geometric_mean.ml		arithmetic_geometric_mean.ml	Removed trailing whitespace in many files	Oct 6, 2021
ballot.ml		ballot.ml	Removed trailing whitespace in many files	Oct 6, 2021
bernoulli.ml		bernoulli.ml	Systematically renamed instances of "&" to "&&" and "or" to "||" to a…	Sep 12, 2016
bertrand.ml		bertrand.ml	Removed trailing whitespace in many files	Oct 6, 2021
birthday.ml		birthday.ml	Initial checkin	Feb 13, 2010
cantor.ml		cantor.ml	Removed trailing whitespace in many files	Oct 6, 2021
cayley_hamilton.ml		cayley_hamilton.ml	Added a proof of invariance of domain in the more general setting of	Feb 17, 2019
ceva.ml		ceva.ml	Initial checkin	Feb 13, 2010
chords.ml		chords.ml	Initial checkin	Feb 13, 2010
circle.ml		circle.ml	Added a variety of very basic real-number and general topology theorems,	Aug 21, 2017
combinations.ml		combinations.ml	Added proofs of the Sylow theorems in a reasonably general form; the	Apr 13, 2020
constructible.ml		constructible.ml	Made the definitions of least common multiples more closely analogous	Mar 15, 2020
cosine.ml		cosine.ml	Initial checkin	Feb 13, 2010
cubic.ml		cubic.ml	Removed trailing whitespace in many files	Oct 6, 2021
derangements.ml		derangements.ml	Initial checkin	Feb 13, 2010
desargues.ml		desargues.ml	Initial checkin	Feb 13, 2010
descartes.ml		descartes.ml	Removed trailing whitespace in many files	Oct 6, 2021
dirichlet.ml		dirichlet.ml	Added a large number of number-theoretic lemmas, mainly trivial but	Dec 23, 2019
div3.ml		div3.ml	Initial checkin	Feb 13, 2010
divharmonic.ml		divharmonic.ml	Initial checkin	Feb 13, 2010
e_is_transcendental.ml		e_is_transcendental.ml	Changed the behaviour of the basic "prove" construct for performing	Aug 1, 2022
euler.ml		euler.ml	Initial checkin	Feb 13, 2010
feuerbach.ml		feuerbach.ml	Added a proof of Feuerbach's theorem.	May 31, 2012
four_squares.ml		four_squares.ml	Added a new Examples file about the NIST-recommended (though see	Mar 1, 2020
fourier.ml		fourier.ml	Separated the material on L_p spaces into its own file Multivariate/l…	Aug 3, 2015
friendship.ml		friendship.ml	Removed trailing whitespace in many files	Oct 6, 2021
fta.ml		fta.ml	Initial checkin	Feb 13, 2010
gcd.ml		gcd.ml	Initial checkin	Feb 13, 2010
heron.ml		heron.ml	Removed trailing whitespace in many files	Oct 6, 2021
inclusion_exclusion.ml		inclusion_exclusion.ml	Eliminated a number of duplicated theorems (often exact duplicates,	Aug 28, 2017
independence.ml		independence.ml	Added proofs of the Sylow theorems in a reasonably general form; the	Apr 13, 2020
isosceles.ml		isosceles.ml	Initial checkin	Feb 13, 2010
konigsberg.ml		konigsberg.ml	Initial checkin	Feb 13, 2010
lagrange.ml		lagrange.ml	Added a new file "Library/grouptheory.ml" with a basic development of	Sep 11, 2017
leibniz.ml		leibniz.ml	Initial checkin	Feb 13, 2010
lhopital.ml		lhopital.ml	Initial checkin	Feb 13, 2010
liouville.ml		liouville.ml	Added a definition of "normal_space" and various properties (including	Jun 5, 2017
minkowski.ml		minkowski.ml	Removed trailing whitespace in many files	Oct 6, 2021
morley.ml		morley.ml	Added a proof of Morley's theorem, following Alain Connes's paper	May 30, 2012
pascal.ml		pascal.ml	Initial checkin	Feb 13, 2010
perfect.ml		perfect.ml	Initial checkin	Feb 13, 2010
pick.ml		pick.ml	Made a modification from Tom Hales to "new_specification", simply usi…	Oct 14, 2013
piseries.ml		piseries.ml	Updated Bill Richter's material, with the topology.ml file now	Feb 18, 2014
platonic.ml		platonic.ml	Added a proof that the Platonic solids are limited to the classic	May 27, 2012
pnt.ml		pnt.ml	Eliminated a number of duplicated theorems (often exact duplicates,	Aug 28, 2017
polyhedron.ml		polyhedron.ml	Added various theorems, mainly Multivariate and in particular a defin…	Aug 22, 2016
primerecip.ml		primerecip.ml	Initial checkin	Feb 13, 2010
ptolemy.ml		ptolemy.ml	Updated Bill Richter's material, with the topology.ml file now	Feb 18, 2014
pythagoras.ml		pythagoras.ml	Initial checkin	Feb 13, 2010
quartic.ml		quartic.ml	Initial checkin	Feb 13, 2010
ramsey.ml		ramsey.ml	Systematically renamed instances of "&" to "&&" and "or" to "||" to a…	Sep 12, 2016
ratcountable.ml		ratcountable.ml	Removed trailing whitespace in many files	Oct 6, 2021
realsuncountable.ml		realsuncountable.ml	Initial checkin	Feb 13, 2010
reciprocity.ml		reciprocity.ml	Added a new library file devoted to Jacobi symbols. The basic NxN->Z	Feb 2, 2020
sqrt.ml		sqrt.ml	Made a radical spring-clean of the general topology and other areas.	Mar 17, 2017
stirling.ml		stirling.ml	Initial checkin	Feb 13, 2010
subsequence.ml		subsequence.ml	Removed trailing whitespace in many files	Oct 6, 2021
thales.ml		thales.ml	Initial checkin	Feb 13, 2010
triangular.ml		triangular.ml	Removed trailing whitespace in many files	Oct 6, 2021
two_squares.ml		two_squares.ml	Added a new Examples file about the NIST-recommended (though see	Mar 1, 2020
wilson.ml		wilson.ml	Added a systematic series of basic definitions and lemmas about	Mar 30, 2020
View all files