summaryrefslogtreecommitdiff
path: root/backends/hol4
ModeNameSize
-rw-r--r--Holmakefile48logplain
-rw-r--r--divDefExampleScript.sml14364logplain
-rw-r--r--divDefExampleTheory.sig5630logplain
-rw-r--r--divDefLib.sig1797logplain
-rw-r--r--divDefLib.sml37473logplain
-rw-r--r--divDefLibTestScript.sml2057logplain
-rw-r--r--divDefLibTestTheory.sig14190logplain
-rw-r--r--divDefNoFixLib.sig3540logplain
-rw-r--r--divDefNoFixLib.sml39447logplain
-rw-r--r--divDefNoFixLibTestScript.sml1582logplain
-rw-r--r--divDefNoFixLibTestTheory.sig12355logplain
-rw-r--r--divDefScript.sml14825logplain
-rw-r--r--divDefTheory.sig6033logplain
-rw-r--r--evalLib.sig988logplain
-rw-r--r--evalLib.sml7861logplain
-rw-r--r--ilistScript.sml3912logplain
-rw-r--r--ilistTheory.sig2728logplain
-rw-r--r--primitivesArithScript.sml10777logplain
-rw-r--r--primitivesArithTheory.sig4922logplain
-rw-r--r--primitivesBaseTacLib.sml25059logplain
-rw-r--r--primitivesLib.sml17869logplain
-rw-r--r--primitivesScript.sml57639logplain
-rw-r--r--primitivesTheory.sig75688logplain
-rw-r--r--saveThmsLib.sig1888logplain
-rw-r--r--saveThmsLib.sml4577logplain
-rw-r--r--testHashmapScript.sml12276logplain
-rw-r--r--testHashmapTheory.sig9091logplain
-rw-r--r--testScript.sml49699logplain
-rw-r--r--testTheory.sig23580logplain