Files

 master

/

src

/

Copy path

Directory actions

More options

Directory actions

More options

Latest commit

myreen

Add a few lemmas to sptreeTheory

Apr 16, 2018

9824ed6 · Apr 16, 2018

History

History

This branch is 5966 commits behind HOL-Theorem-Prover/HOL:master.

/

src

/

Top

Folders and files

Name		Name	Last commit message	Last commit date
parent directory ..
0		0	Standard and experimental kernels now share Thm.sml implementation	Jan 10, 2018
1		1	Generate "standard" datatype simpl rewrites as tyinfos are loaded	Apr 16, 2018
Boolify		Boolify	Fix Boolify/Encode	Mar 22, 2018
HolQbf		HolQbf	Protect some Unicode in a .sig file's comments	Sep 15, 2016
HolSat		HolSat	Remove some stale redeclarations of things like THEN1 and >-	Sep 6, 2017
HolSmt		HolSmt	Improving naming of bit-vector signed division constants.	Sep 11, 2017
IndDef		IndDef	Up to core types	Mar 19, 2018
TeX		TeX	Provide >>~ option to munging commands	Apr 10, 2018
bag		bag	Re-implement Datatype package with TypeBase sexps (not adjoin)	Apr 12, 2018
basicProof		basicProof	Remove an unnecessary ref in BasicProvers.sml	Oct 13, 2017
bool		bool	Record width=3 for standard TeX iff (⇔), which is suprisingly huge	Apr 10, 2018
boss		boss	Fix (unused?) ml_evaluation/Lift.{sig,sml}	Mar 28, 2018
coalgebras		coalgebras	Use TypeBase.export to avoid adjoin_to_theory calls	Apr 9, 2018
combin		combin	Fix for (new, pretty branch) bug causing computeLib failures with K	Mar 27, 2018
compute		compute	Re-implement Datatype package with TypeBase sexps (not adjoin)	Apr 12, 2018
coretypes		coretypes	Generate "standard" datatype simpl rewrites as tyinfos are loaded	Apr 16, 2018
datatype		datatype	Generate "standard" datatype simpl rewrites as tyinfos are loaded	Apr 16, 2018
emit		emit	Change emitted numML to use PP.pretty rather than PP.ppstream	Mar 25, 2018
enumfset		enumfset	Fixed building of totoTacs.sml in mosml (after 93036c7)	Jul 22, 2017
experimental-kernel		experimental-kernel	Make experimental kernel's term representation visible to Thm	Jan 10, 2018
finite_map		finite_map	Fixes of bag, container, finite_map and in n-bit/	Mar 21, 2018
float		float	Remove -- as an alias for Term parser.	Oct 3, 2017
floating-point		floating-point	Check for signalling NaNs in floating-point conversions.	Nov 29, 2017
hol88		hol88	Removed further functions from hol88Lib.	Sep 21, 2009
holyhammer		holyhammer	holyhammer: export problem with no predictions for ltb	Apr 12, 2018
integer		integer	Re-implement Datatype package with TypeBase sexps (not adjoin)	Apr 12, 2018
list		list	Re-implement Datatype package with TypeBase sexps (not adjoin)	Apr 12, 2018
lite		lite	extra semicolons removed from (some) .sig files	Feb 10, 2015
marker		marker	Make PAT_ABBREV_TAC aware of hidden/revealed status of "constants"	Jul 17, 2017
meson		meson	code style: space after parenthesis in "(x*y)list"	Feb 10, 2015
metis		metis	Up to core types	Mar 19, 2018
monad		monad	Restore ppstream_funs as nullary type operator in term_pp_types	Mar 29, 2018
n-bit		n-bit	Restore ppstream_funs as nullary type operator in term_pp_types	Mar 29, 2018
new-datatype		new-datatype	Delete trailing whitespace in src/	Nov 26, 2015
num		num	Generate "standard" datatype simpl rewrites as tyinfos are loaded	Apr 16, 2018
opentheory		opentheory	Make OpenTheory Logging more robust to uptodate	Apr 28, 2017
parse		parse	Fix terrible performance when reading large strings with Coding	Apr 14, 2018
patricia		patricia	Add a few lemmas to sptreeTheory	Apr 16, 2018
pattern_matches		pattern_matches	Make patternMatchesLib use a specified parsing context	Apr 13, 2018
pfl		pfl	saving before an update	Dec 6, 2015
portableML		portableML	Changes to get Moscow ML impl. to build once more	Mar 28, 2018
postkernel		postkernel	Don't save already saved thms when writing them out to ThyDataSexps	Apr 16, 2018
pred_set		pred_set	Re-implement Datatype package with TypeBase sexps (not adjoin)	Apr 12, 2018
prekernel		prekernel	Fix terrible performance when reading large strings with Coding	Apr 14, 2018
probability		probability	Move FINITE_BIJ_COUNT_EQ to pred_setTheory to simplify FINITE_BIJ_COU…	Jul 31, 2017
proofman		proofman	Tweaks to goal pretty-printing along with tests	Apr 3, 2018
q		q	Provide access to more switches when parsing in context	Jul 17, 2017
quantHeuristics		quantHeuristics	Use Unicode quotes in some self-test output	Jun 27, 2017
quotient		quotient	Remove -- as an alias for Term parser.	Oct 3, 2017
rational		rational	Untabify src/rational/ratLib.sml	Jan 13, 2018
real		real	Fix topologyScript, which shouldn't have been using adjoin at all	Mar 22, 2018
refute		refute	Make dependencies for refute's selftest more accurate	Oct 27, 2017
relation		relation	Added TeX notation for relation inversion (relinv)	Dec 1, 2017
res_quan		res_quan	Avoid spurious theory dependencies in Poly/ML with heap numheap.	Oct 23, 2017
ring		ring	Fix src/ring/src	Mar 22, 2018
search		search	Avoid warning message when loading dftTheory.	Aug 8, 2016
simp		simp	Up to core types	Mar 19, 2018
sort		sort	Remove -- as an alias for Term parser.	Oct 3, 2017
string		string	Builds core HOL; quotient fails for lack of (temporary) html_theory	Mar 20, 2018
tactictoe		tactictoe	tactictoe: fix if then else arguments in org_tac	Apr 12, 2018
taut		taut	Moved documentation from src/*/help/entries directories to help/Docfi…	Aug 6, 2010
temporal		temporal	Remove -- as an alias for Term parser.	Oct 3, 2017
tfl		tfl	Builds core HOL; quotient fails for lack of (temporary) html_theory	Mar 20, 2018
thm		thm	Move smpp to Portable - get everything up to arithmeticScript working	Mar 20, 2018
transfer		transfer	More results about the finite-map/sptree connection	Sep 22, 2017
unwind		unwind	Fixed 'make clean' for several LaTeX results.	Jul 31, 2014
update		update	Modify the type of HolKernel.syntax_fns and add some documentation.	May 11, 2015
View all files