https://github.com/JacquesCarette/hol-light
Tip revision: b27a524086caf73530b7c2c5da1b237d3539f143 authored by Jacques Carette on 24 August 2020, 14:18:07 UTC
Merge pull request #35 from sjjs7/final-changes
Merge pull request #35 from sjjs7/final-changes
Tip revision: b27a524
| File | Mode | Size |
|---|---|---|
| 100 | ||
| Arithmetic | ||
| Boyer_Moore | ||
| Complex | ||
| Constructions | ||
| Examples | ||
| Formal_ineqs | ||
| Functionspaces | ||
| 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 | ||
| .gitattributes | -rw-r--r-- | 57 bytes |
| .gitignore | -rw-r--r-- | 58 bytes |
| CHANGES | -rw-r--r-- | 763.8 KB |
| LICENSE | -rw-r--r-- | 1.6 KB |
| Makefile | -rw-r--r-- | 8.9 KB |
| QUICK_REFERENCE.txt | -rw-r--r-- | 90.5 KB |
| README | -rw-r--r-- | 1.7 KB |
| README-hol-light | -rw-r--r-- | 10.9 KB |
| VERYQUICK_REFERENCE.txt | -rw-r--r-- | 19.3 KB |
| all_diffs.txt | -rw-r--r-- | 151.5 KB |
| arith.ml | -rw-r--r-- | 72.4 KB |
| basics.ml | -rw-r--r-- | 17.9 KB |
| bool.ml | -rw-r--r-- | 17.2 KB |
| boot.ml | -rw-r--r-- | 360 bytes |
| calc_int.ml | -rw-r--r-- | 14.7 KB |
| calc_num.ml | -rw-r--r-- | 66.6 KB |
| calc_rat.ml | -rw-r--r-- | 27.9 KB |
| canon.ml | -rw-r--r-- | 33.1 KB |
| cart.ml | -rw-r--r-- | 28.9 KB |
| class.ml | -rw-r--r-- | 19.6 KB |
| compute.ml | -rw-r--r-- | 27.7 KB |
| database.ml | -rw-r--r-- | 88.8 KB |
| define.ml | -rw-r--r-- | 46.0 KB |
| doc-to-help.sed | -rw-r--r-- | 971 bytes |
| drule.ml | -rw-r--r-- | 24.4 KB |
| equal.ml | -rw-r--r-- | 13.4 KB |
| firstorder.ml | -rw-r--r-- | 8.2 KB |
| fusion.ml | -rw-r--r-- | 70.5 KB |
| grobner.ml | -rw-r--r-- | 33.1 KB |
| help.ml | -rw-r--r-- | 5.7 KB |
| hol.ml | -rw-r--r-- | 9.0 KB |
| holQE.ml | -rw-r--r-- | 890 bytes |
| holtest | -rwxr-xr-x | 17.9 KB |
| holtest.mk | -rw-r--r-- | 7.5 KB |
| holtest_parallel | -rwxr-xr-x | 1.2 KB |
| impconv.ml | -rw-r--r-- | 65.6 KB |
| ind_defs.ml | -rw-r--r-- | 19.9 KB |
| ind_types.ml | -rw-r--r-- | 70.9 KB |
| int.ml | -rw-r--r-- | 102.7 KB |
| itab.ml | -rw-r--r-- | 3.8 KB |
| iterate.ml | -rw-r--r-- | 128.6 KB |
| lib.ml | -rw-r--r-- | 28.8 KB |
| lists.ml | -rw-r--r-- | 30.5 KB |
| make.ml | -rw-r--r-- | 2.5 KB |
| meson.ml | -rw-r--r-- | 35.9 KB |
| metis.ml | -rw-r--r-- | 331.0 KB |
| nets.ml | -rw-r--r-- | 6.3 KB |
| normalizer.ml | -rw-r--r-- | 24.4 KB |
| nums.ml | -rw-r--r-- | 13.5 KB |
| pa_j_3.07.ml | -rw-r--r-- | 83.3 KB |
| pa_j_3.08.ml | -rw-r--r-- | 75.9 KB |
| pa_j_3.09.ml | -rw-r--r-- | 77.0 KB |
| pa_j_3.1x_5.xx.ml | -rw-r--r-- | 67.5 KB |
| pa_j_3.1x_6.02.1.ml | -rw-r--r-- | 94.7 KB |
| pa_j_3.1x_6.02.2.ml | -rw-r--r-- | 94.6 KB |
| pa_j_3.1x_6.11.ml | -rw-r--r-- | 98.5 KB |
| pa_j_3.1x_6.xx.ml | -rw-r--r-- | 94.6 KB |
| pa_j_4.xx_7.06.ml | -rw-r--r-- | 98.6 KB |
| pa_j_4.xx_7.xx.ml | -rwxr-xr-x | 98.6 KB |
| pair.ml | -rw-r--r-- | 19.2 KB |
| parser.ml | -rw-r--r-- | 24.0 KB |
| preterm.ml | -rw-r--r-- | 21.3 KB |
| printer.ml | -rw-r--r-- | 25.7 KB |
| quot.ml | -rw-r--r-- | 8.0 KB |
| real.ml | -rw-r--r-- | 68.3 KB |
| realarith.ml | -rw-r--r-- | 25.6 KB |
| realax.ml | -rw-r--r-- | 87.2 KB |
| recursion.ml | -rw-r--r-- | 5.5 KB |
| sets.ml | -rw-r--r-- | 197.7 KB |
| simp.ml | -rw-r--r-- | 26.6 KB |
| system.ml | -rw-r--r-- | 2.6 KB |
| tactics.ml | -rw-r--r-- | 35.7 KB |
| thecops.ml | -rw-r--r-- | 53.4 KB |
| theorems.ml | -rw-r--r-- | 20.2 KB |
| trivia.ml | -rw-r--r-- | 3.4 KB |
| update_database_3.ml | -rwxr-xr-x | 8.8 KB |
| update_database_4.ml | -rwxr-xr-x | 8.5 KB |
| wf.ml | -rw-r--r-- | 20.2 KB |
