https://github.com/jrh13/hol-light
Tip revision: 016d22698294583153a0d9ff625d0b0cf44ee9d1 authored by jrh13 on 08 August 2024, 17:37:10 UTC
Merge pull request #106 from aqjune-aws/bugfix
Merge pull request #106 from aqjune-aws/bugfix
Tip revision: 016d226
| File | Mode | Size |
|---|---|---|
| .github | ||
| 100 | ||
| Arithmetic | ||
| Boyer_Moore | ||
| Cadical | ||
| Complex | ||
| Divstep | ||
| EC | ||
| Examples | ||
| Formal_ineqs | ||
| Functionspaces | ||
| GL | ||
| Geometric_Algebra | ||
| Help | ||
| IEEE | ||
| IsabelleLight | ||
| Jordan | ||
| LP_arith | ||
| Library | ||
| Logic | ||
| Minisat | ||
| Mizarlight | ||
| Model | ||
| Multivariate | ||
| Ntrie | ||
| Permutation | ||
| ProofTrace | ||
| Proofrecording | ||
| QBF | ||
| Quaternions | ||
| RichterHilbertAxiomGeometry | ||
| Rqe | ||
| Tutorial | ||
| Unity | ||
| miz3 | ||
| pa_j | ||
| .gitattributes | -rw-r--r-- | 57 bytes |
| .gitignore | -rw-r--r-- | 82 bytes |
| CHANGES | -rw-r--r-- | 988.8 KB |
| LICENSE | -rw-r--r-- | 1.6 KB |
| Makefile | -rw-r--r-- | 10.5 KB |
| QUICK_REFERENCE.txt | -rw-r--r-- | 90.5 KB |
| README | -rw-r--r-- | 9.8 KB |
| VERYQUICK_REFERENCE.txt | -rw-r--r-- | 19.3 KB |
| arith.ml | -rw-r--r-- | 73.7 KB |
| basics.ml | -rwxr-xr-x | 17.6 KB |
| bignum_num.ml | -rw-r--r-- | 636 bytes |
| bignum_zarith.ml | -rw-r--r-- | 3.6 KB |
| bool.ml | -rw-r--r-- | 17.4 KB |
| calc_int.ml | -rw-r--r-- | 14.8 KB |
| calc_num.ml | -rw-r--r-- | 68.1 KB |
| calc_rat.ml | -rw-r--r-- | 28.0 KB |
| canon.ml | -rw-r--r-- | 33.1 KB |
| cart.ml | -rw-r--r-- | 29.7 KB |
| class.ml | -rwxr-xr-x | 19.7 KB |
| compute.ml | -rw-r--r-- | 27.7 KB |
| database.ml | -rw-r--r-- | 91.0 KB |
| define.ml | -rw-r--r-- | 44.7 KB |
| doc-to-help.sed | -rw-r--r-- | 971 bytes |
| drule.ml | -rw-r--r-- | 23.7 KB |
| equal.ml | -rw-r--r-- | 12.2 KB |
| firstorder.ml | -rw-r--r-- | 8.2 KB |
| fusion.ml | -rw-r--r-- | 27.9 KB |
| grobner.ml | -rw-r--r-- | 33.1 KB |
| help.ml | -rwxr-xr-x | 5.7 KB |
| hol.ml | -rw-r--r-- | 10.5 KB |
| hol_4.14.sh | -rwxr-xr-x | 554 bytes |
| hol_4.sh | -rwxr-xr-x | 598 bytes |
| holtest | -rwxr-xr-x | 18.0 KB |
| holtest.mk | -rw-r--r-- | 8.3 KB |
| holtest_parallel | -rwxr-xr-x | 1.2 KB |
| impconv.ml | -rw-r--r-- | 64.6 KB |
| ind_defs.ml | -rw-r--r-- | 19.9 KB |
| ind_types.ml | -rwxr-xr-x | 71.1 KB |
| int.ml | -rwxr-xr-x | 113.6 KB |
| itab.ml | -rw-r--r-- | 3.8 KB |
| iterate.ml | -rw-r--r-- | 128.7 KB |
| lib.ml | -rwxr-xr-x | 28.9 KB |
| lists.ml | -rw-r--r-- | 31.5 KB |
| load_camlp4.ml | -rw-r--r-- | 54 bytes |
| load_camlp5.ml | -rw-r--r-- | 88 bytes |
| load_camlp5_topfind.ml | -rw-r--r-- | 324 bytes |
| make.ml | -rw-r--r-- | 2.5 KB |
| meson.ml | -rw-r--r-- | 36.1 KB |
| metis.ml | -rw-r--r-- | 331.0 KB |
| nets.ml | -rw-r--r-- | 5.5 KB |
| normalizer.ml | -rw-r--r-- | 24.4 KB |
| nums.ml | -rw-r--r-- | 13.5 KB |
| pair.ml | -rwxr-xr-x | 20.0 KB |
| parser.ml | -rw-r--r-- | 23.4 KB |
| preterm.ml | -rw-r--r-- | 20.0 KB |
| printer.ml | -rwxr-xr-x | 25.9 KB |
| quot.ml | -rw-r--r-- | 8.0 KB |
| real.ml | -rw-r--r-- | 69.0 KB |
| realarith.ml | -rw-r--r-- | 26.5 KB |
| realax.ml | -rw-r--r-- | 87.2 KB |
| recursion.ml | -rw-r--r-- | 5.5 KB |
| sets.ml | -rw-r--r-- | 205.3 KB |
| simp.ml | -rw-r--r-- | 24.1 KB |
| system.ml | -rw-r--r-- | 1.2 KB |
| tactics.ml | -rw-r--r-- | 36.7 KB |
| thecops.ml | -rw-r--r-- | 53.4 KB |
| theorems.ml | -rwxr-xr-x | 20.2 KB |
| trivia.ml | -rw-r--r-- | 3.4 KB |
| update_database_3.ml | -rwxr-xr-x | 8.8 KB |
| update_database_4.14.ml | -rwxr-xr-x | 5.5 KB |
| update_database_4.ml | -rwxr-xr-x | 8.5 KB |
| update_database_5.ml | -rwxr-xr-x | 1.2 KB |
| wf.ml | -rw-r--r-- | 20.3 KB |
