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.sig14076logplain
-rw-r--r--divDefNoFixLib.sig3540logplain
-rw-r--r--divDefNoFixLib.sml39444logplain
-rw-r--r--divDefNoFixLibTestScript.sml1582logplain
-rw-r--r--divDefNoFixLibTestTheory.sig12217logplain
-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.sml10498logplain
-rw-r--r--primitivesArithTheory.sig4922logplain
-rw-r--r--primitivesBaseTacLib.sml25542logplain
-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