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 |
|---|---|---|
| asym.ml | -rw-r--r-- | 83.9 KB |
| basic.ml | -rw-r--r-- | 1.0 KB |
| condense.ml | -rw-r--r-- | 19.8 KB |
| condense_thms.ml | -rw-r--r-- | 1.5 KB |
| dedmatrix.ml | -rw-r--r-- | 9.3 KB |
| dedmatrix_thms.ml | -rw-r--r-- | 3.6 KB |
| defs.ml | -rw-r--r-- | 9.4 KB |
| examples.ml | -rw-r--r-- | 38.6 KB |
| inferisign.ml | -rw-r--r-- | 8.8 KB |
| inferisign_thms.ml | -rw-r--r-- | 27.1 KB |
| inferpsign.ml | -rw-r--r-- | 13.0 KB |
| inferpsign_thms.ml | -rw-r--r-- | 11.5 KB |
| lift_qelim.ml | -rw-r--r-- | 4.7 KB |
| list_rewrites.ml | -rw-r--r-- | 721 bytes |
| main_thms.ml | -rw-r--r-- | 7.9 KB |
| make.ml | -rw-r--r-- | 1.5 KB |
| matinsert.ml | -rw-r--r-- | 3.7 KB |
| matinsert_thms.ml | -rw-r--r-- | 129 bytes |
| num_calc_simp.ml | -rw-r--r-- | 1.8 KB |
| pdivides.ml | -rw-r--r-- | 3.4 KB |
| pdivides_thms.ml | -rw-r--r-- | 1.4 KB |
| poly_ext.ml | -rw-r--r-- | 26.2 KB |
| rewrites.ml | -rw-r--r-- | 1.7 KB |
| rol.ml | -rw-r--r-- | 16.3 KB |
| rqe_lib.ml | -rw-r--r-- | 3.6 KB |
| rqe_list.ml | -rw-r--r-- | 6.7 KB |
| rqe_main.ml | -rw-r--r-- | 22.9 KB |
| rqe_num.ml | -rw-r--r-- | 892 bytes |
| rqe_real.ml | -rw-r--r-- | 11.6 KB |
| rqe_tactics_ext.ml | -rw-r--r-- | 8.2 KB |
| signs.ml | -rw-r--r-- | 11.3 KB |
| signs_thms.ml | -rw-r--r-- | 3.6 KB |
| simplify.ml | -rw-r--r-- | 5.1 KB |
| testform.ml | -rw-r--r-- | 9.5 KB |
| testform_thms.ml | -rw-r--r-- | 7.1 KB |
| timers.ml | -rw-r--r-- | 2.4 KB |
| util.ml | -rw-r--r-- | 3.0 KB |
| work_thms.ml | -rw-r--r-- | 282.0 KB |
