data/hol-light-20190729/CHANGES:2360: consequentially ==> consequently
data/hol-light-20190729/CHANGES:4028: parantheses ==> parentheses
data/hol-light-20190729/CHANGES:4833: vesion ==> version
data/hol-light-20190729/CHANGES:4878: stricly ==> strictly
data/hol-light-20190729/CHANGES:5472: Addded ==> Added
data/hol-light-20190729/CHANGES:5700: Archimedian ==> Archimedean
data/hol-light-20190729/CHANGES:5963: cacheing ==> caching
data/hol-light-20190729/CHANGES:6388: Archimedian ==> Archimedean
data/hol-light-20190729/CHANGES:8456: Slighly ==> Slightly
data/hol-light-20190729/CHANGES:8681: slighly ==> slightly
data/hol-light-20190729/CHANGES:9062: cacheing ==> caching
data/hol-light-20190729/CHANGES:10143: Decomissioned ==> Decommissioned
data/hol-light-20190729/CHANGES:10863: upto ==> up to
data/hol-light-20190729/CHANGES:12301: upto ==> up to
data/hol-light-20190729/CHANGES:12729: sepearated ==> separated
data/hol-light-20190729/CHANGES:12758: overriden ==> overridden
data/hol-light-20190729/CHANGES:13081: atleast ==> at least
data/hol-light-20190729/CHANGES:13159: contructing ==> constructing
data/hol-light-20190729/CHANGES:13926: Archimedian ==> Archimedean
data/hol-light-20190729/CHANGES:14149: upto ==> up to
data/hol-light-20190729/CHANGES:14151: upto ==> up to
data/hol-light-20190729/CHANGES:14152: upto ==> up to
data/hol-light-20190729/CHANGES:14492: maching ==> machine, marching, matching
data/hol-light-20190729/CHANGES:15174: savable ==> saveable
data/hol-light-20190729/CHANGES:15198: Chaged ==> Changed, charged
data/hol-light-20190729/CHANGES:15487: aci ==> acpi
data/hol-light-20190729/CHANGES:15544: ISTS ==> ITS, LISTS
data/hol-light-20190729/CHANGES:15869: delting ==> deleting
data/hol-light-20190729/CHANGES:16752: cacheing ==> caching
data/hol-light-20190729/CHANGES:16788: cacheing ==> caching
data/hol-light-20190729/CHANGES:16808: consequentially ==> consequently
data/hol-light-20190729/CHANGES:16836: defalt ==> default
data/hol-light-20190729/CHANGES:16836: consequentially ==> consequently
data/hol-light-20190729/QUICK_REFERENCE.txt:134: ths ==> the, this
data/hol-light-20190729/QUICK_REFERENCE.txt:256: ths ==> the, this
data/hol-light-20190729/QUICK_REFERENCE.txt:259: ths ==> the, this
data/hol-light-20190729/QUICK_REFERENCE.txt:319: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:320: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:322: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:323: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:323: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:348: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:350: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:352: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:354: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:356: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:358: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:367: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:367: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:370: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:370: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:471: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:472: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:472: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:478: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:479: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:480: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:482: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:483: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:486: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:487: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:489: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:490: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:497: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:498: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:500: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:501: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:514: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:515: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:518: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:530: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:532: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:534: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:538: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:540: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:542: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:543: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:641: strat ==> start, strata
data/hol-light-20190729/QUICK_REFERENCE.txt:643: strat ==> start, strata
data/hol-light-20190729/QUICK_REFERENCE.txt:673: strat ==> start, strata
data/hol-light-20190729/QUICK_REFERENCE.txt:676: strat ==> start, strata
data/hol-light-20190729/QUICK_REFERENCE.txt:677: strat ==> start, strata
data/hol-light-20190729/QUICK_REFERENCE.txt:678: strat ==> start, strata
data/hol-light-20190729/QUICK_REFERENCE.txt:683: strat ==> start, strata
data/hol-light-20190729/QUICK_REFERENCE.txt:686: strat ==> start, strata
data/hol-light-20190729/QUICK_REFERENCE.txt:690: strat ==> start, strata
data/hol-light-20190729/QUICK_REFERENCE.txt:696: strat ==> start, strata
data/hol-light-20190729/QUICK_REFERENCE.txt:698: strat ==> start, strata
data/hol-light-20190729/QUICK_REFERENCE.txt:702: strat ==> start, strata
data/hol-light-20190729/QUICK_REFERENCE.txt:704: strat ==> start, strata
data/hol-light-20190729/QUICK_REFERENCE.txt:707: strat ==> start, strata
data/hol-light-20190729/QUICK_REFERENCE.txt:708: strat ==> start, strata
data/hol-light-20190729/QUICK_REFERENCE.txt:769: ths ==> the, this
data/hol-light-20190729/QUICK_REFERENCE.txt:799: strat ==> start, strata
data/hol-light-20190729/QUICK_REFERENCE.txt:801: strat ==> start, strata
data/hol-light-20190729/QUICK_REFERENCE.txt:1179: tht ==> the, that
data/hol-light-20190729/QUICK_REFERENCE.txt:1179: tht ==> the, that
data/hol-light-20190729/README:75: Somtimes ==> Sometimes
data/hol-light-20190729/arith.ml:15: intensional ==> intentional
data/hol-light-20190729/calc_rat.ml:600: ths ==> the, this
data/hol-light-20190729/calc_rat.ml:601: ths ==> the, this
data/hol-light-20190729/calc_rat.ml:608: ths ==> the, this
data/hol-light-20190729/calc_rat.ml:609: ths ==> the, this
data/hol-light-20190729/canon.ml:24: ACI ==> ACPI
data/hol-light-20190729/class.ml:428: intensionally ==> intentionally
data/hol-light-20190729/compute.ml:117: tha ==> than, that, the
data/hol-light-20190729/compute.ml:118: tha ==> than, that, the
data/hol-light-20190729/compute.ml:121: tha ==> than, that, the
data/hol-light-20190729/compute.ml:122: tha ==> than, that, the
data/hol-light-20190729/compute.ml:198: CLOS ==> CLOSE
data/hol-light-20190729/compute.ml:205: immediatly ==> immediately
data/hol-light-20190729/compute.ml:221: Clos ==> Close
data/hol-light-20190729/compute.ml:490: succesfully ==> successfully
data/hol-light-20190729/compute.ml:561: Clos ==> Close
data/hol-light-20190729/compute.ml:592: insted ==> instead
data/hol-light-20190729/compute.ml:593: insted ==> instead
data/hol-light-20190729/compute.ml:622: tha ==> than, that, the
data/hol-light-20190729/compute.ml:622: tha ==> than, that, the
data/hol-light-20190729/compute.ml:648: Clos ==> Close
data/hol-light-20190729/compute.ml:649: tha ==> than, that, the
data/hol-light-20190729/compute.ml:650: tha ==> than, that, the
data/hol-light-20190729/compute.ml:651: Clos ==> Close
data/hol-light-20190729/compute.ml:654: clos ==> close
data/hol-light-20190729/compute.ml:655: clos ==> close
data/hol-light-20190729/compute.ml:655: clos ==> close
data/hol-light-20190729/compute.ml:656: clos ==> close
data/hol-light-20190729/compute.ml:656: clos ==> close
data/hol-light-20190729/compute.ml:670: clos ==> close
data/hol-light-20190729/compute.ml:671: clos ==> close
data/hol-light-20190729/compute.ml:677: clos ==> close
data/hol-light-20190729/compute.ml:677: clos ==> close
data/hol-light-20190729/compute.ml:686: Clos ==> Close
data/hol-light-20190729/compute.ml:689: Clos ==> Close
data/hol-light-20190729/compute.ml:700: tha ==> than, that, the
data/hol-light-20190729/compute.ml:701: tha ==> than, that, the
data/hol-light-20190729/compute.ml:702: clos ==> close
data/hol-light-20190729/compute.ml:704: clos ==> close
data/hol-light-20190729/compute.ml:705: clos ==> close
data/hol-light-20190729/compute.ml:706: tha ==> than, that, the
data/hol-light-20190729/compute.ml:707: tha ==> than, that, the
data/hol-light-20190729/define.ml:713: parms ==> params, prams
data/hol-light-20190729/define.ml:714: parm ==> param, pram, parma
data/hol-light-20190729/define.ml:714: parms ==> params, prams
data/hol-light-20190729/define.ml:716: parm ==> param, pram, parma
data/hol-light-20190729/define.ml:716: parm ==> param, pram, parma
data/hol-light-20190729/define.ml:717: parm ==> param, pram, parma
data/hol-light-20190729/define.ml:718: parm ==> param, pram, parma
data/hol-light-20190729/define.ml:721: parms ==> params, prams
data/hol-light-20190729/define.ml:721: parms ==> params, prams
data/hol-light-20190729/define.ml:729: parm ==> param, pram, parma
data/hol-light-20190729/define.ml:729: parms ==> params, prams
data/hol-light-20190729/define.ml:730: parm ==> param, pram, parma
data/hol-light-20190729/define.ml:731: parms ==> params, prams
data/hol-light-20190729/define.ml:731: parm ==> param, pram, parma
data/hol-light-20190729/define.ml:732: parms ==> params, prams
data/hol-light-20190729/define.ml:764: parms ==> params, prams
data/hol-light-20190729/define.ml:765: parm ==> param, pram, parma
data/hol-light-20190729/define.ml:765: parms ==> params, prams
data/hol-light-20190729/define.ml:766: parm ==> param, pram, parma
data/hol-light-20190729/define.ml:768: parm ==> param, pram, parma
data/hol-light-20190729/define.ml:774: parms ==> params, prams
data/hol-light-20190729/define.ml:776: parm ==> param, pram, parma
data/hol-light-20190729/define.ml:776: parms ==> params, prams
data/hol-light-20190729/define.ml:824: parms ==> params, prams
data/hol-light-20190729/define.ml:835: parms ==> params, prams
data/hol-light-20190729/define.ml:837: parms ==> params, prams
data/hol-light-20190729/define.ml:944: wth ==> with
data/hol-light-20190729/define.ml:945: wth ==> with
data/hol-light-20190729/define.ml:971: ths ==> the, this
data/hol-light-20190729/define.ml:972: ths ==> the, this
data/hol-light-20190729/define.ml:974: ths ==> the, this
data/hol-light-20190729/drule.ml:536: ths ==> the, this
data/hol-light-20190729/drule.ml:537: ths ==> the, this
data/hol-light-20190729/equal.ml:306: ths ==> the, this
data/hol-light-20190729/equal.ml:307: ths ==> the, this
data/hol-light-20190729/equal.ml:308: ths ==> the, this
data/hol-light-20190729/equal.ml:314: ths ==> the, this
data/hol-light-20190729/equal.ml:326: ths ==> the, this
data/hol-light-20190729/equal.ml:326: ths ==> the, this
data/hol-light-20190729/firstorder.ml:213: FOF ==> FOR
data/hol-light-20190729/firstorder.ml:216: FO ==> OF, FOR
data/hol-light-20190729/grobner.ml:127: hist ==> heist, his
data/hol-light-20190729/grobner.ml:129: hist ==> heist, his
data/hol-light-20190729/grobner.ml:131: hist ==> heist, his
data/hol-light-20190729/grobner.ml:133: hist ==> heist, his
data/hol-light-20190729/grobner.ml:161: hist ==> heist, his
data/hol-light-20190729/grobner.ml:162: hist ==> heist, his
data/hol-light-20190729/grobner.ml:165: hist ==> heist, his
data/hol-light-20190729/grobner.ml:223: hist ==> heist, his
data/hol-light-20190729/grobner.ml:576: parms ==> params, prams
data/hol-light-20190729/grobner.ml:576: parms ==> params, prams
data/hol-light-20190729/grobner.ml:578: parms ==> params, prams
data/hol-light-20190729/grobner.ml:578: parms ==> params, prams
data/hol-light-20190729/help.ml:24: upto ==> up to
data/hol-light-20190729/impconv.ml:545: ba ==> by, be
data/hol-light-20190729/impconv.ml:546: ba ==> by, be
data/hol-light-20190729/impconv.ml:570: ba ==> by, be
data/hol-light-20190729/impconv.ml:571: ba ==> by, be
data/hol-light-20190729/impconv.ml:723: ba ==> by, be
data/hol-light-20190729/impconv.ml:724: ba ==> by, be
data/hol-light-20190729/impconv.ml:1307: ths ==> the, this
data/hol-light-20190729/impconv.ml:1308: ths ==> the, this
data/hol-light-20190729/impconv.ml:1318: ths ==> the, this
data/hol-light-20190729/impconv.ml:1319: ths ==> the, this
data/hol-light-20190729/impconv.ml:1320: ths ==> the, this
data/hol-light-20190729/impconv.ml:1322: ths ==> the, this
data/hol-light-20190729/impconv.ml:1324: ths ==> the, this
data/hol-light-20190729/impconv.ml:1324: ths ==> the, this
data/hol-light-20190729/impconv.ml:1327: ths ==> the, this
data/hol-light-20190729/impconv.ml:1329: ths ==> the, this
data/hol-light-20190729/impconv.ml:1329: ths ==> the, this
data/hol-light-20190729/impconv.ml:1329: ths ==> the, this
data/hol-light-20190729/impconv.ml:1339: withouth ==> without
data/hol-light-20190729/impconv.ml:1390: ths ==> the, this
data/hol-light-20190729/impconv.ml:1391: ths ==> the, this
data/hol-light-20190729/impconv.ml:1393: ths ==> the, this
data/hol-light-20190729/impconv.ml:1395: ths ==> the, this
data/hol-light-20190729/impconv.ml:1400: ths ==> the, this
data/hol-light-20190729/impconv.ml:1596: ths ==> the, this
data/hol-light-20190729/impconv.ml:1597: ths ==> the, this
data/hol-light-20190729/impconv.ml:1658: ths ==> the, this
data/hol-light-20190729/impconv.ml:1659: ths ==> the, this
data/hol-light-20190729/impconv.ml:1681: ths ==> the, this
data/hol-light-20190729/impconv.ml:1682: ths ==> the, this
data/hol-light-20190729/impconv.ml:1693: ths ==> the, this
data/hol-light-20190729/impconv.ml:1695: ths ==> the, this
data/hol-light-20190729/impconv.ml:1697: ths ==> the, this
data/hol-light-20190729/impconv.ml:1697: ths ==> the, this
data/hol-light-20190729/impconv.ml:1700: ths ==> the, this
data/hol-light-20190729/impconv.ml:1702: ths ==> the, this
data/hol-light-20190729/impconv.ml:1703: ths ==> the, this
data/hol-light-20190729/impconv.ml:1703: ths ==> the, this
data/hol-light-20190729/impconv.ml:1825: ths ==> the, this
data/hol-light-20190729/impconv.ml:1826: ths ==> the, this
data/hol-light-20190729/impconv.ml:1845: ths ==> the, this
data/hol-light-20190729/impconv.ml:1847: ths ==> the, this
data/hol-light-20190729/impconv.ml:1848: ths ==> the, this
data/hol-light-20190729/ind_defs.ml:67: ths ==> the, this
data/hol-light-20190729/ind_defs.ml:68: ths ==> the, this
data/hol-light-20190729/ind_defs.ml:69: ths ==> the, this
data/hol-light-20190729/ind_defs.ml:75: tht ==> the, that
data/hol-light-20190729/ind_defs.ml:75: ths ==> the, this
data/hol-light-20190729/ind_defs.ml:78: tht ==> the, that
data/hol-light-20190729/ind_defs.ml:114: ths ==> the, this
data/hol-light-20190729/ind_defs.ml:115: ths ==> the, this
data/hol-light-20190729/ind_defs.ml:129: ths ==> the, this
data/hol-light-20190729/ind_defs.ml:130: ths ==> the, this
data/hol-light-20190729/ind_defs.ml:393: ths ==> the, this
data/hol-light-20190729/ind_defs.ml:394: ths ==> the, this
data/hol-light-20190729/ind_types.ml:406: ths ==> the, this
data/hol-light-20190729/ind_types.ml:409: ths ==> the, this
data/hol-light-20190729/ind_types.ml:418: ths ==> the, this
data/hol-light-20190729/ind_types.ml:491: ba ==> by, be
data/hol-light-20190729/ind_types.ml:502: ths ==> the, this
data/hol-light-20190729/ind_types.ml:503: ths ==> the, this
data/hol-light-20190729/ind_types.ml:566: ths ==> the, this
data/hol-light-20190729/ind_types.ml:567: ths ==> the, this
data/hol-light-20190729/ind_types.ml:966: ths ==> the, this
data/hol-light-20190729/ind_types.ml:967: ths ==> the, this
data/hol-light-20190729/ind_types.ml:968: ths ==> the, this
data/hol-light-20190729/ind_types.ml:1262: ths ==> the, this
data/hol-light-20190729/ind_types.ml:1263: ths ==> the, this
data/hol-light-20190729/int.ml:707: Archimedian ==> Archimedean
data/hol-light-20190729/int.ml:1688: ths ==> the, this
data/hol-light-20190729/int.ml:1690: ths ==> the, this
data/hol-light-20190729/lib.ml:544: analagous ==> analogous
data/hol-light-20190729/meson.ml:281: Cacheing ==> Caching
data/hol-light-20190729/meson.ml:567: ths ==> the, this
data/hol-light-20190729/meson.ml:571: ths ==> the, this
data/hol-light-20190729/meson.ml:571: ths ==> the, this
data/hol-light-20190729/meson.ml:671: lits ==> list
data/hol-light-20190729/meson.ml:672: lits ==> list
data/hol-light-20190729/meson.ml:709: ths ==> the, this
data/hol-light-20190729/meson.ml:710: ths ==> the, this
data/hol-light-20190729/meson.ml:713: ths ==> the, this
data/hol-light-20190729/meson.ml:714: ths ==> the, this
data/hol-light-20190729/meson.ml:715: ths ==> the, this
data/hol-light-20190729/meson.ml:716: ths ==> the, this
data/hol-light-20190729/meson.ml:719: ths ==> the, this
data/hol-light-20190729/meson.ml:758: ths ==> the, this
data/hol-light-20190729/meson.ml:759: ths ==> the, this
data/hol-light-20190729/meson.ml:760: ths ==> the, this
data/hol-light-20190729/meson.ml:762: ths ==> the, this
data/hol-light-20190729/meson.ml:763: ths ==> the, this
data/hol-light-20190729/meson.ml:765: ths ==> the, this
data/hol-light-20190729/meson.ml:772: ths ==> the, this
data/hol-light-20190729/meson.ml:777: ths ==> the, this
data/hol-light-20190729/meson.ml:778: ths ==> the, this
data/hol-light-20190729/meson.ml:778: ths ==> the, this
data/hol-light-20190729/meson.ml:810: ths ==> the, this
data/hol-light-20190729/meson.ml:812: ths ==> the, this
data/hol-light-20190729/meson.ml:841: ths ==> the, this
data/hol-light-20190729/meson.ml:841: ths ==> the, this
data/hol-light-20190729/meson.ml:847: ths ==> the, this
data/hol-light-20190729/meson.ml:847: ths ==> the, this
data/hol-light-20190729/metis.ml:3945: lits ==> list
data/hol-light-20190729/metis.ml:3945: lits ==> list
data/hol-light-20190729/metis.ml:3962: lits ==> list
data/hol-light-20190729/metis.ml:3969: lits ==> list
data/hol-light-20190729/metis.ml:3971: lits ==> list
data/hol-light-20190729/metis.ml:4100: ths ==> the, this
data/hol-light-20190729/metis.ml:4103: ths ==> the, this
data/hol-light-20190729/metis.ml:4111: ths ==> the, this
data/hol-light-20190729/metis.ml:4117: ths ==> the, this
data/hol-light-20190729/metis.ml:4271: lits ==> list
data/hol-light-20190729/metis.ml:4275: lits ==> list
data/hol-light-20190729/metis.ml:4295: lits ==> list
data/hol-light-20190729/metis.ml:4297: lits ==> list
data/hol-light-20190729/metis.ml:4297: lits ==> list
data/hol-light-20190729/metis.ml:4434: ths ==> the, this
data/hol-light-20190729/metis.ml:4437: ths ==> the, this
data/hol-light-20190729/metis.ml:4437: ths ==> the, this
data/hol-light-20190729/metis.ml:4440: ths ==> the, this
data/hol-light-20190729/metis.ml:4440: ths ==> the, this
data/hol-light-20190729/metis.ml:4442: ths ==> the, this
data/hol-light-20190729/metis.ml:4442: ths ==> the, this
data/hol-light-20190729/metis.ml:4443: ths ==> the, this
data/hol-light-20190729/metis.ml:4447: ths ==> the, this
data/hol-light-20190729/metis.ml:4450: ths ==> the, this
data/hol-light-20190729/metis.ml:4451: ths ==> the, this
data/hol-light-20190729/metis.ml:4454: ths ==> the, this
data/hol-light-20190729/metis.ml:4454: ths ==> the, this
data/hol-light-20190729/metis.ml:4455: ths ==> the, this
data/hol-light-20190729/metis.ml:4455: ths ==> the, this
data/hol-light-20190729/metis.ml:4458: ths ==> the, this
data/hol-light-20190729/metis.ml:4460: ths ==> the, this
data/hol-light-20190729/metis.ml:4461: ths ==> the, this
data/hol-light-20190729/metis.ml:4461: ths ==> the, this
data/hol-light-20190729/metis.ml:4463: ths ==> the, this
data/hol-light-20190729/metis.ml:4471: ths ==> the, this
data/hol-light-20190729/metis.ml:4472: ths ==> the, this
data/hol-light-20190729/metis.ml:4487: lits ==> list
data/hol-light-20190729/metis.ml:4487: lits ==> list
data/hol-light-20190729/metis.ml:4502: lits ==> list
data/hol-light-20190729/metis.ml:4502: lits ==> list
data/hol-light-20190729/metis.ml:4934: lits ==> list
data/hol-light-20190729/metis.ml:4934: lits ==> list
data/hol-light-20190729/metis.ml:5201: lits ==> list
data/hol-light-20190729/metis.ml:5202: lits ==> list
data/hol-light-20190729/metis.ml:5210: lits ==> list
data/hol-light-20190729/metis.ml:5214: lits ==> list
data/hol-light-20190729/metis.ml:6535: parm ==> param, pram, parma
data/hol-light-20190729/metis.ml:6535: parm ==> param, pram, parma
data/hol-light-20190729/metis.ml:6587: parm ==> param, pram, parma
data/hol-light-20190729/metis.ml:6587: parm ==> param, pram, parma
data/hol-light-20190729/metis.ml:6724: parm ==> param, pram, parma
data/hol-light-20190729/metis.ml:6724: parm ==> param, pram, parma
data/hol-light-20190729/metis.ml:6780: parm ==> param, pram, parma
data/hol-light-20190729/metis.ml:6781: parm ==> param, pram, parma
data/hol-light-20190729/metis.ml:6812: parm ==> param, pram, parma
data/hol-light-20190729/metis.ml:6813: parm ==> param, pram, parma
data/hol-light-20190729/metis.ml:6855: parm ==> param, pram, parma
data/hol-light-20190729/metis.ml:6855: parm ==> param, pram, parma
data/hol-light-20190729/metis.ml:6901: parm ==> param, pram, parma
data/hol-light-20190729/metis.ml:6901: parm ==> param, pram, parma
data/hol-light-20190729/metis.ml:6901: parm ==> param, pram, parma
data/hol-light-20190729/metis.ml:6918: parm ==> param, pram, parma
data/hol-light-20190729/metis.ml:6918: parm ==> param, pram, parma
data/hol-light-20190729/metis.ml:6978: lits ==> list
data/hol-light-20190729/metis.ml:6978: lits ==> list
data/hol-light-20190729/metis.ml:6978: lits ==> list
data/hol-light-20190729/metis.ml:6982: lits ==> list
data/hol-light-20190729/metis.ml:6984: lits ==> list
data/hol-light-20190729/metis.ml:6988: lits ==> list
data/hol-light-20190729/metis.ml:6990: lits ==> list
data/hol-light-20190729/metis.ml:7160: lits ==> list
data/hol-light-20190729/metis.ml:7161: lits ==> list
data/hol-light-20190729/metis.ml:7242: lits ==> list
data/hol-light-20190729/metis.ml:7244: lits ==> list
data/hol-light-20190729/metis.ml:7606: lits ==> list
data/hol-light-20190729/metis.ml:7607: lits ==> list
data/hol-light-20190729/metis.ml:7734: lits ==> list
data/hol-light-20190729/metis.ml:7736: lits ==> list
data/hol-light-20190729/metis.ml:7737: lits ==> list
data/hol-light-20190729/metis.ml:7780: lits ==> list
data/hol-light-20190729/metis.ml:7783: lits ==> list
data/hol-light-20190729/metis.ml:7792: lits ==> list
data/hol-light-20190729/metis.ml:7793: lits ==> list
data/hol-light-20190729/metis.ml:7795: lits ==> list
data/hol-light-20190729/metis.ml:7796: lits ==> list
data/hol-light-20190729/metis.ml:7797: lits ==> list
data/hol-light-20190729/metis.ml:7799: lits ==> list
data/hol-light-20190729/metis.ml:7800: lits ==> list
data/hol-light-20190729/metis.ml:7802: lits ==> list
data/hol-light-20190729/metis.ml:7802: lits ==> list
data/hol-light-20190729/metis.ml:7804: lits ==> list
data/hol-light-20190729/metis.ml:7804: lits ==> list
data/hol-light-20190729/metis.ml:7812: lits ==> list
data/hol-light-20190729/metis.ml:8050: ths ==> the, this
data/hol-light-20190729/metis.ml:8052: ths ==> the, this
data/hol-light-20190729/metis.ml:8067: ths ==> the, this
data/hol-light-20190729/metis.ml:8068: ths ==> the, this
data/hol-light-20190729/metis.ml:8278: lits ==> list
data/hol-light-20190729/metis.ml:8284: lits ==> list
data/hol-light-20190729/metis.ml:8288: lits ==> list
data/hol-light-20190729/metis.ml:8294: lits ==> list
data/hol-light-20190729/metis.ml:8404: lits ==> list
data/hol-light-20190729/metis.ml:8408: lits ==> list
data/hol-light-20190729/metis.ml:8807: lits ==> list
data/hol-light-20190729/metis.ml:8809: lits ==> list
data/hol-light-20190729/metis.ml:8810: lits ==> list
data/hol-light-20190729/metis.ml:9028: lits ==> list
data/hol-light-20190729/metis.ml:9033: lits ==> list
data/hol-light-20190729/metis.ml:9033: lits ==> list
data/hol-light-20190729/metis.ml:9046: lits ==> list
data/hol-light-20190729/metis.ml:9444: lits ==> list
data/hol-light-20190729/metis.ml:9445: lits ==> list
data/hol-light-20190729/metis.ml:9447: lits ==> list
data/hol-light-20190729/metis.ml:9468: parm ==> param, pram, parma
data/hol-light-20190729/metis.ml:9469: parm ==> param, pram, parma
data/hol-light-20190729/metis.ml:9477: parms ==> params, prams
data/hol-light-20190729/metis.ml:9478: parm ==> param, pram, parma
data/hol-light-20190729/metis.ml:9479: parm ==> param, pram, parma
data/hol-light-20190729/metis.ml:9485: parms ==> params, prams
data/hol-light-20190729/metis.ml:9488: parms ==> params, prams
data/hol-light-20190729/metis.ml:9489: parm ==> param, pram, parma
data/hol-light-20190729/metis.ml:9490: parm ==> param, pram, parma
data/hol-light-20190729/metis.ml:9494: parms ==> params, prams
data/hol-light-20190729/metis.ml:9510: parm ==> param, pram, parma
data/hol-light-20190729/metis.ml:9514: parm ==> param, pram, parma
data/hol-light-20190729/metis.ml:9515: lits ==> list
data/hol-light-20190729/metis.ml:9516: lits ==> list
data/hol-light-20190729/metis.ml:9517: lits ==> list
data/hol-light-20190729/metis.ml:9518: lits ==> list
data/hol-light-20190729/metis.ml:9669: ths ==> the, this
data/hol-light-20190729/metis.ml:9672: ths ==> the, this
data/hol-light-20190729/metis.ml:9672: ths ==> the, this
data/hol-light-20190729/metis.ml:9766: ths ==> the, this
data/hol-light-20190729/metis.ml:9767: ths ==> the, this
data/hol-light-20190729/metis.ml:10263: ths ==> the, this
data/hol-light-20190729/metis.ml:10273: ths ==> the, this
data/hol-light-20190729/metis.ml:10278: thn ==> then
data/hol-light-20190729/metis.ml:10284: thn ==> then
data/hol-light-20190729/metis.ml:10341: ths ==> the, this
data/hol-light-20190729/metis.ml:10346: ths ==> the, this
data/hol-light-20190729/metis.ml:10349: ths ==> the, this
data/hol-light-20190729/metis.ml:10350: ths ==> the, this
data/hol-light-20190729/metis.ml:10354: ths ==> the, this
data/hol-light-20190729/metis.ml:10354: ths ==> the, this
data/hol-light-20190729/metis.ml:10355: ths ==> the, this
data/hol-light-20190729/metis.ml:10358: ths ==> the, this
data/hol-light-20190729/metis.ml:10359: ths ==> the, this
data/hol-light-20190729/metis.ml:10364: ths ==> the, this
data/hol-light-20190729/metis.ml:10374: ths ==> the, this
data/hol-light-20190729/metis.ml:10375: ths ==> the, this
data/hol-light-20190729/metis.ml:10386: ths ==> the, this
data/hol-light-20190729/metis.ml:10386: ths ==> the, this
data/hol-light-20190729/metis.ml:10388: ths ==> the, this
data/hol-light-20190729/metis.ml:10388: ths ==> the, this
data/hol-light-20190729/pa_j_3.07.ml:6: Cristal ==> Crystal
data/hol-light-20190729/pa_j_3.07.ml:1175: upto ==> up to
data/hol-light-20190729/pa_j_3.07.ml:2390: upto ==> up to
data/hol-light-20190729/pa_j_3.07.ml:2390: upto ==> up to
data/hol-light-20190729/pa_j_3.08.ml:6: Cristal ==> Crystal
data/hol-light-20190729/pa_j_3.08.ml:936: upto ==> up to
data/hol-light-20190729/pa_j_3.08.ml:2167: upto ==> up to
data/hol-light-20190729/pa_j_3.08.ml:2167: upto ==> up to
data/hol-light-20190729/pa_j_3.09.ml:6: Cristal ==> Crystal
data/hol-light-20190729/pa_j_3.09.ml:974: upto ==> up to
data/hol-light-20190729/pa_j_3.09.ml:2193: upto ==> up to
data/hol-light-20190729/pa_j_3.09.ml:2193: upto ==> up to
data/hol-light-20190729/pa_j_3.1x_5.xx.ml:832: upto ==> up to
data/hol-light-20190729/pa_j_3.1x_5.xx.ml:2008: upto ==> up to
data/hol-light-20190729/pa_j_3.1x_5.xx.ml:2008: upto ==> up to
data/hol-light-20190729/pa_j_3.1x_6.02.1.ml:366: ExTry ==> entry
data/hol-light-20190729/pa_j_3.1x_6.02.1.ml:368: ExTry ==> entry
data/hol-light-20190729/pa_j_3.1x_6.02.1.ml:1583: upto ==> up to
data/hol-light-20190729/pa_j_3.1x_6.02.1.ml:2844: upto ==> up to
data/hol-light-20190729/pa_j_3.1x_6.02.1.ml:2844: upto ==> up to
data/hol-light-20190729/pa_j_3.1x_6.02.2.ml:362: ExTry ==> entry
data/hol-light-20190729/pa_j_3.1x_6.02.2.ml:364: ExTry ==> entry
data/hol-light-20190729/pa_j_3.1x_6.02.2.ml:1565: upto ==> up to
data/hol-light-20190729/pa_j_3.1x_6.02.2.ml:2826: upto ==> up to
data/hol-light-20190729/pa_j_3.1x_6.02.2.ml:2826: upto ==> up to
data/hol-light-20190729/pa_j_3.1x_6.11.ml:375: ExTry ==> entry
data/hol-light-20190729/pa_j_3.1x_6.11.ml:377: ExTry ==> entry
data/hol-light-20190729/pa_j_3.1x_6.11.ml:1641: upto ==> up to
data/hol-light-20190729/pa_j_3.1x_6.11.ml:2949: upto ==> up to
data/hol-light-20190729/pa_j_3.1x_6.11.ml:2949: upto ==> up to
data/hol-light-20190729/pa_j_3.1x_6.xx.ml:360: ExTry ==> entry
data/hol-light-20190729/pa_j_3.1x_6.xx.ml:362: ExTry ==> entry
data/hol-light-20190729/pa_j_3.1x_6.xx.ml:1577: upto ==> up to
data/hol-light-20190729/pa_j_3.1x_6.xx.ml:2838: upto ==> up to
data/hol-light-20190729/pa_j_3.1x_6.xx.ml:2838: upto ==> up to
data/hol-light-20190729/pa_j_4.xx_7.06.ml:378: ExTry ==> entry
data/hol-light-20190729/pa_j_4.xx_7.06.ml:380: ExTry ==> entry
data/hol-light-20190729/pa_j_4.xx_7.06.ml:1644: upto ==> up to
data/hol-light-20190729/pa_j_4.xx_7.06.ml:2952: upto ==> up to
data/hol-light-20190729/pa_j_4.xx_7.06.ml:2952: upto ==> up to
data/hol-light-20190729/pair.ml:241: ths ==> the, this
data/hol-light-20190729/pair.ml:242: ths ==> the, this
data/hol-light-20190729/pair.ml:242: ths ==> the, this
data/hol-light-20190729/pair.ml:258: ths ==> the, this
data/hol-light-20190729/pair.ml:261: ths ==> the, this
data/hol-light-20190729/parser.ml:78: atleast ==> at least
data/hol-light-20190729/parser.ml:80: atleast ==> at least
data/hol-light-20190729/parser.ml:109: atleast ==> at least
data/hol-light-20190729/quot.ml:65: wth ==> with
data/hol-light-20190729/quot.ml:66: wth ==> with
data/hol-light-20190729/quot.ml:108: wth ==> with
data/hol-light-20190729/real.ml:1418: Archimedian ==> Archimedean
data/hol-light-20190729/realarith.ml:330: ths ==> the, this
data/hol-light-20190729/realarith.ml:331: ths ==> the, this
data/hol-light-20190729/realax.ml:1229: ths ==> the, this
data/hol-light-20190729/realax.ml:1231: ths ==> the, this
data/hol-light-20190729/recursion.ml:57: ths ==> the, this
data/hol-light-20190729/recursion.ml:58: ths ==> the, this
data/hol-light-20190729/recursion.ml:60: ths ==> the, this
data/hol-light-20190729/sets.ml:261: ths ==> the, this
data/hol-light-20190729/sets.ml:262: ths ==> the, this
data/hol-light-20190729/sets.ml:262: ths ==> the, this
data/hol-light-20190729/simp.ml:171: ths ==> the, this
data/hol-light-20190729/simp.ml:173: ths ==> the, this
data/hol-light-20190729/simp.ml:174: ths ==> the, this
data/hol-light-20190729/simp.ml:229: strat ==> start, strata
data/hol-light-20190729/simp.ml:230: strat ==> start, strata
data/hol-light-20190729/simp.ml:278: strat ==> start, strata
data/hol-light-20190729/simp.ml:286: strat ==> start, strata
data/hol-light-20190729/simp.ml:288: strat ==> start, strata
data/hol-light-20190729/simp.ml:297: strat ==> start, strata
data/hol-light-20190729/simp.ml:302: strat ==> start, strata
data/hol-light-20190729/simp.ml:304: strat ==> start, strata
data/hol-light-20190729/simp.ml:308: strat ==> start, strata
data/hol-light-20190729/simp.ml:312: strat ==> start, strata
data/hol-light-20190729/simp.ml:313: strat ==> start, strata
data/hol-light-20190729/simp.ml:315: strat ==> start, strata
data/hol-light-20190729/simp.ml:318: strat ==> start, strata
data/hol-light-20190729/simp.ml:322: strat ==> start, strata
data/hol-light-20190729/simp.ml:376: Maintenence ==> Maintenance
data/hol-light-20190729/simp.ml:492: strat ==> start, strata
data/hol-light-20190729/simp.ml:494: strat ==> start, strata
data/hol-light-20190729/tactics.ml:120: ths ==> the, this
data/hol-light-20190729/tactics.ml:121: ths ==> the, this
data/hol-light-20190729/tactics.ml:136: ths ==> the, this
data/hol-light-20190729/tactics.ml:137: ths ==> the, this
data/hol-light-20190729/tactics.ml:148: ths ==> the, this
data/hol-light-20190729/tactics.ml:149: ths ==> the, this
data/hol-light-20190729/tactics.ml:305: ths ==> the, this
data/hol-light-20190729/tactics.ml:305: ths ==> the, this
data/hol-light-20190729/tactics.ml:601: ths ==> the, this
data/hol-light-20190729/tactics.ml:603: ths ==> the, this
data/hol-light-20190729/tactics.ml:814: ths ==> the, this
data/hol-light-20190729/tactics.ml:816: ths ==> the, this
data/hol-light-20190729/tactics.ml:828: ths ==> the, this
data/hol-light-20190729/tactics.ml:829: ths ==> the, this
data/hol-light-20190729/tactics.ml:829: ths ==> the, this
data/hol-light-20190729/tactics.ml:834: ths ==> the, this
data/hol-light-20190729/tactics.ml:835: ths ==> the, this
data/hol-light-20190729/tactics.ml:835: ths ==> the, this
data/hol-light-20190729/thecops.ml:240: ths ==> the, this
data/hol-light-20190729/thecops.ml:242: ths ==> the, this
data/hol-light-20190729/thecops.ml:255: iterm ==> term, item, intern
data/hol-light-20190729/thecops.ml:269: iterm ==> term, item, intern
data/hol-light-20190729/thecops.ml:269: iterm ==> term, item, intern
data/hol-light-20190729/thecops.ml:270: iterm ==> term, item, intern
data/hol-light-20190729/thecops.ml:270: iterm ==> term, item, intern
data/hol-light-20190729/thecops.ml:272: iterm ==> term, item, intern
data/hol-light-20190729/thecops.ml:272: iterm ==> term, item, intern
data/hol-light-20190729/thecops.ml:276: iterm ==> term, item, intern
data/hol-light-20190729/thecops.ml:279: iterm ==> term, item, intern
data/hol-light-20190729/thecops.ml:284: iterm ==> term, item, intern
data/hol-light-20190729/thecops.ml:350: iterm ==> term, item, intern
data/hol-light-20190729/thecops.ml:414: iterm ==> term, item, intern
data/hol-light-20190729/thecops.ml:585: ths ==> the, this
data/hol-light-20190729/thecops.ml:588: ths ==> the, this
data/hol-light-20190729/thecops.ml:681: lits ==> list
data/hol-light-20190729/thecops.ml:687: lits ==> list
data/hol-light-20190729/thecops.ml:710: ths ==> the, this
data/hol-light-20190729/thecops.ml:713: ths ==> the, this
data/hol-light-20190729/thecops.ml:713: ths ==> the, this
data/hol-light-20190729/thecops.ml:749: ths ==> the, this
data/hol-light-20190729/thecops.ml:751: ths ==> the, this
data/hol-light-20190729/thecops.ml:751: ths ==> the, this
data/hol-light-20190729/thecops.ml:759: ths ==> the, this
data/hol-light-20190729/thecops.ml:760: ths ==> the, this
data/hol-light-20190729/thecops.ml:771: ths ==> the, this
data/hol-light-20190729/thecops.ml:771: ths ==> the, this
data/hol-light-20190729/thecops.ml:772: ths ==> the, this
data/hol-light-20190729/thecops.ml:772: ths ==> the, this
data/hol-light-20190729/thecops.ml:773: ths ==> the, this
data/hol-light-20190729/thecops.ml:773: ths ==> the, this
data/hol-light-20190729/thecops.ml:1020: matC ==> match
data/hol-light-20190729/thecops.ml:1024: matC ==> match
data/hol-light-20190729/thecops.ml:1071: matC ==> match
data/hol-light-20190729/thecops.ml:1072: matC ==> match
data/hol-light-20190729/thecops.ml:1074: matC ==> match
data/hol-light-20190729/thecops.ml:1342: thi ==> the, this
data/hol-light-20190729/thecops.ml:1345: thi ==> the, this
data/hol-light-20190729/thecops.ml:1349: thi ==> the, this
data/hol-light-20190729/thecops.ml:1349: thi ==> the, this
data/hol-light-20190729/thecops.ml:1352: thi ==> the, this
data/hol-light-20190729/thecops.ml:1356: thi ==> the, this
data/hol-light-20190729/thecops.ml:1360: thi ==> the, this
data/hol-light-20190729/thecops.ml:1369: thi ==> the, this
data/hol-light-20190729/thecops.ml:1370: thi ==> the, this
data/hol-light-20190729/thecops.ml:1373: thi ==> the, this
data/hol-light-20190729/thecops.ml:1429: ths ==> the, this
data/hol-light-20190729/thecops.ml:1431: ths ==> the, this
data/hol-light-20190729/thecops.ml:1432: ths ==> the, this
data/hol-light-20190729/thecops.ml:1437: ths ==> the, this
data/hol-light-20190729/thecops.ml:1438: ths ==> the, this
data/hol-light-20190729/thecops.ml:1438: ths ==> the, this
data/hol-light-20190729/thecops.ml:1465: ths ==> the, this
data/hol-light-20190729/thecops.ml:1466: ths ==> the, this
data/hol-light-20190729/thecops.ml:1474: ths ==> the, this
data/hol-light-20190729/thecops.ml:1474: ths ==> the, this
data/hol-light-20190729/thecops.ml:1476: ths ==> the, this
data/hol-light-20190729/thecops.ml:1476: ths ==> the, this
data/hol-light-20190729/thecops.ml:1477: ths ==> the, this
data/hol-light-20190729/thecops.ml:1477: ths ==> the, this
data/hol-light-20190729/theorems.ml:483: atleast ==> at least
data/hol-light-20190729/theorems.ml:486: atleast ==> at least
data/hol-light-20190729/holtest_parallel:40: follwing ==> following
data/hol-light-20190729/pa_j_4.xx_7.xx.ml:378: ExTry ==> entry
data/hol-light-20190729/pa_j_4.xx_7.xx.ml:380: ExTry ==> entry
data/hol-light-20190729/pa_j_4.xx_7.xx.ml:1646: upto ==> up to
data/hol-light-20190729/pa_j_4.xx_7.xx.ml:2957: upto ==> up to
data/hol-light-20190729/pa_j_4.xx_7.xx.ml:2957: upto ==> up to
data/hol-light-20190729/100/bertrand.ml:15: ommission ==> omission
data/hol-light-20190729/100/bertrand.ml:1069: ths ==> the, this
data/hol-light-20190729/100/bertrand.ml:1071: ths ==> the, this
data/hol-light-20190729/100/bertrand.ml:1074: ths ==> the, this
data/hol-light-20190729/100/bertrand.ml:1497: ths ==> the, this
data/hol-light-20190729/100/bertrand.ml:1499: ths ==> the, this
data/hol-light-20190729/100/bertrand.ml:1500: ths ==> the, this
data/hol-light-20190729/100/bertrand.ml:2563: ths ==> the, this
data/hol-light-20190729/100/bertrand.ml:2565: ths ==> the, this
data/hol-light-20190729/100/bertrand.ml:2566: ths ==> the, this
data/hol-light-20190729/100/constructible.ml:183: expresion ==> expression
data/hol-light-20190729/100/e_is_transcendental.ml:62: Bolean ==> Boolean
data/hol-light-20190729/100/e_is_transcendental.ml:1375: ths ==> the, this
data/hol-light-20190729/100/e_is_transcendental.ml:1376: ths ==> the, this
data/hol-light-20190729/100/e_is_transcendental.ml:2121: alwasy ==> always
data/hol-light-20190729/100/e_is_transcendental.ml:2199: suprisingly ==> surprisingly
data/hol-light-20190729/100/pnt.ml:13: miscelleneous ==> miscellaneous
data/hol-light-20190729/100/ramsey.ml:260: thi ==> the, this
data/hol-light-20190729/100/ramsey.ml:261: thi ==> the, this
data/hol-light-20190729/100/ramsey.ml:262: thi ==> the, this
data/hol-light-20190729/100/ramsey.ml:263: thi ==> the, this
data/hol-light-20190729/100/ramsey.ml:470: ths ==> the, this
data/hol-light-20190729/100/ramsey.ml:472: ths ==> the, this
data/hol-light-20190729/100/ramsey.ml:473: ths ==> the, this
data/hol-light-20190729/100/ramsey.ml:635: ths ==> the, this
data/hol-light-20190729/100/ramsey.ml:638: ths ==> the, this
data/hol-light-20190729/100/ramsey.ml:644: ths ==> the, this
data/hol-light-20190729/100/ramsey.ml:645: ths ==> the, this
data/hol-light-20190729/100/ramsey.ml:737: ths ==> the, this
data/hol-light-20190729/100/ramsey.ml:737: ths ==> the, this
data/hol-light-20190729/Arithmetic/definability.ml:464: ths ==> the, this
data/hol-light-20190729/Arithmetic/definability.ml:465: ths ==> the, this
data/hol-light-20190729/Arithmetic/derived.ml:892: ths ==> the, this
data/hol-light-20190729/Arithmetic/derived.ml:896: ths ==> the, this
data/hol-light-20190729/Arithmetic/godel.ml:249: ths ==> the, this
data/hol-light-20190729/Arithmetic/godel.ml:251: ths ==> the, this
data/hol-light-20190729/Arithmetic/godel.ml:253: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/environment.ml:87: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/environment.ml:88: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/environment.ml:91: hashI ==> hash
data/hol-light-20190729/Boyer_Moore/environment.ml:139: antecedant ==> antecedent
data/hol-light-20190729/Boyer_Moore/equalities.ml:149: hashI ==> hash
data/hol-light-20190729/Boyer_Moore/equalities.ml:150: hashI ==> hash
data/hol-light-20190729/Boyer_Moore/generalize.ml:400: occurences ==> occurrences
data/hol-light-20190729/Boyer_Moore/generalize.ml:401: occurences ==> occurrences
data/hol-light-20190729/Boyer_Moore/induction.ml:126: antecedant ==> antecedent
data/hol-light-20190729/Boyer_Moore/induction.ml:144: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/induction.ml:146: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/induction.ml:149: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/struct_equal.ml:48: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/struct_equal.ml:49: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/struct_equal.ml:52: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/struct_equal.ml:55: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/struct_equal.ml:56: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/struct_equal.ml:142: hashI ==> hash
data/hol-light-20190729/Boyer_Moore/struct_equal.ml:228: rotats ==> rotates, rotate
data/hol-light-20190729/Boyer_Moore/struct_equal.ml:230: rotats ==> rotates, rotate
data/hol-light-20190729/Boyer_Moore/support.ml:24: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/support.ml:26: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/support.ml:27: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/support.ml:55: hashI ==> hash
data/hol-light-20190729/Boyer_Moore/terms_and_clauses.ml:71: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/terms_and_clauses.ml:72: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/terms_and_clauses.ml:74: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/terms_and_clauses.ml:77: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/terms_and_clauses.ml:651: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/terms_and_clauses.ml:656: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/terms_and_clauses.ml:656: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/terms_and_clauses.ml:664: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/terms_and_clauses.ml:664: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/terms_and_clauses.ml:676: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:59: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:61: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:62: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:77: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:82: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:84: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:85: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:245: hashI ==> hash
data/hol-light-20190729/Boyer_Moore/waterfall.ml:266: hashI ==> hash
data/hol-light-20190729/Boyer_Moore/waterfall.ml:296: hashI ==> hash
data/hol-light-20190729/Boyer_Moore/waterfall.ml:326: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:328: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:329: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:330: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:333: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:336: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:338: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:340: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:342: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:344: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:348: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:350: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:351: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:352: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:355: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:358: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:360: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:362: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:364: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:366: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:487: hashI ==> hash
data/hol-light-20190729/Boyer_Moore/waterfall.ml:552: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:554: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:568: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:569: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:654: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:701: ths ==> the, this
data/hol-light-20190729/Boyer_Moore/waterfall.ml:706: ths ==> the, this
data/hol-light-20190729/Complex/complex_grobner.ml:148: hist ==> heist, his
data/hol-light-20190729/Complex/complex_grobner.ml:150: hist ==> heist, his
data/hol-light-20190729/Complex/complex_grobner.ml:152: hist ==> heist, his
data/hol-light-20190729/Complex/complex_grobner.ml:154: hist ==> heist, his
data/hol-light-20190729/Complex/complex_grobner.ml:182: hist ==> heist, his
data/hol-light-20190729/Complex/complex_grobner.ml:183: hist ==> heist, his
data/hol-light-20190729/Complex/complex_grobner.ml:186: hist ==> heist, his
data/hol-light-20190729/Complex/complex_grobner.ml:243: hist ==> heist, his
data/hol-light-20190729/Complex/complex_grobner.ml:248: hist ==> heist, his
data/hol-light-20190729/Complex/complex_grobner.ml:253: hist ==> heist, his
data/hol-light-20190729/Complex/complex_grobner.ml:432: ths ==> the, this
data/hol-light-20190729/Complex/complex_grobner.ml:435: ths ==> the, this
data/hol-light-20190729/Complex/complex_grobner.ml:449: ths ==> the, this
data/hol-light-20190729/Complex/complex_grobner.ml:451: ths ==> the, this
data/hol-light-20190729/Complex/complex_grobner.ml:451: ths ==> the, this
data/hol-light-20190729/Complex/complexnumbers.ml:867: ths ==> the, this
data/hol-light-20190729/Complex/complexnumbers.ml:868: ths ==> the, this
data/hol-light-20190729/Complex/complexnumbers.ml:869: ths ==> the, this
data/hol-light-20190729/Complex/complexnumbers.ml:875: ths ==> the, this
data/hol-light-20190729/Complex/complexnumbers.ml:876: ths ==> the, this
data/hol-light-20190729/Complex/quelim.ml:792: tha ==> than, that, the
data/hol-light-20190729/Complex/quelim.ml:794: tha ==> than, that, the
data/hol-light-20190729/Complex/quelim.ml:837: ths ==> the, this
data/hol-light-20190729/Complex/quelim.ml:838: ths ==> the, this
data/hol-light-20190729/Examples/combin.ml:4: develoment ==> development
data/hol-light-20190729/Examples/digit_serial_methods.ml:10: extravagent ==> extravagant
data/hol-light-20190729/Examples/digit_serial_methods.ml:677: ths ==> the, this
data/hol-light-20190729/Examples/digit_serial_methods.ml:679: ths ==> the, this
data/hol-light-20190729/Examples/digit_serial_methods.ml:680: ths ==> the, this
data/hol-light-20190729/Examples/hol88.ml:5: upto ==> up to
data/hol-light-20190729/Examples/hol88.ml:360: thi ==> the, this
data/hol-light-20190729/Examples/hol88.ml:361: thi ==> the, this
data/hol-light-20190729/Examples/hol88.ml:362: thi ==> the, this
data/hol-light-20190729/Examples/hol88.ml:363: thi ==> the, this
data/hol-light-20190729/Examples/hol88.ml:570: ths ==> the, this
data/hol-light-20190729/Examples/hol88.ml:572: ths ==> the, this
data/hol-light-20190729/Examples/hol88.ml:573: ths ==> the, this
data/hol-light-20190729/Examples/hol88.ml:653: ths ==> the, this
data/hol-light-20190729/Examples/hol88.ml:654: ths ==> the, this
data/hol-light-20190729/Examples/hol88.ml:659: ths ==> the, this
data/hol-light-20190729/Examples/hol88.ml:668: ths ==> the, this
data/hol-light-20190729/Examples/hol88.ml:668: ths ==> the, this
data/hol-light-20190729/Examples/hol88.ml:753: ths ==> the, this
data/hol-light-20190729/Examples/hol88.ml:757: ths ==> the, this
data/hol-light-20190729/Examples/hol88.ml:763: ths ==> the, this
data/hol-light-20190729/Examples/hol88.ml:764: ths ==> the, this
data/hol-light-20190729/Examples/hol88.ml:888: ths ==> the, this
data/hol-light-20190729/Examples/hol88.ml:888: ths ==> the, this
data/hol-light-20190729/Examples/holby.ml:161: ths ==> the, this
data/hol-light-20190729/Examples/holby.ml:162: ths ==> the, this
data/hol-light-20190729/Examples/holby.ml:163: thn ==> then
data/hol-light-20190729/Examples/holby.ml:163: thn ==> then
data/hol-light-20190729/Examples/holby.ml:174: ths ==> the, this
data/hol-light-20190729/Examples/holby.ml:174: ths ==> the, this
data/hol-light-20190729/Examples/holby.ml:176: ths ==> the, this
data/hol-light-20190729/Examples/holby.ml:354: ths ==> the, this
data/hol-light-20190729/Examples/holby.ml:355: ths ==> the, this
data/hol-light-20190729/Examples/holby.ml:550: ths ==> the, this
data/hol-light-20190729/Examples/holby.ml:554: ths ==> the, this
data/hol-light-20190729/Examples/holby.ml:558: ths ==> the, this
data/hol-light-20190729/Examples/holby.ml:564: ths ==> the, this
data/hol-light-20190729/Examples/holby.ml:565: ths ==> the, this
data/hol-light-20190729/Examples/holby.ml:607: ths ==> the, this
data/hol-light-20190729/Examples/holby.ml:608: ths ==> the, this
data/hol-light-20190729/Examples/holby.ml:620: thn ==> then
data/hol-light-20190729/Examples/holby.ml:621: thn ==> then
data/hol-light-20190729/Examples/holby.ml:622: thn ==> then
data/hol-light-20190729/Examples/holby.ml:636: ths ==> the, this
data/hol-light-20190729/Examples/holby.ml:636: ths ==> the, this
data/hol-light-20190729/Examples/holby.ml:644: ths ==> the, this
data/hol-light-20190729/Examples/holby.ml:647: ths ==> the, this
data/hol-light-20190729/Examples/holby.ml:669: ths ==> the, this
data/hol-light-20190729/Examples/holby.ml:670: ths ==> the, this
data/hol-light-20190729/Examples/holby.ml:671: ths ==> the, this
data/hol-light-20190729/Examples/holby.ml:675: ths ==> the, this
data/hol-light-20190729/Examples/holby.ml:679: ths ==> the, this
data/hol-light-20190729/Examples/holby.ml:682: ths ==> the, this
data/hol-light-20190729/Examples/kb.ml:94: ths ==> the, this
data/hol-light-20190729/Examples/kb.ml:94: ths ==> the, this
data/hol-light-20190729/Examples/kb.ml:131: ths ==> the, this
data/hol-light-20190729/Examples/kb.ml:133: ths ==> the, this
data/hol-light-20190729/Examples/kb.ml:133: ths ==> the, this
data/hol-light-20190729/Examples/kb.ml:134: ths ==> the, this
data/hol-light-20190729/Examples/kb.ml:137: tha ==> than, that, the
data/hol-light-20190729/Examples/kb.ml:138: tha ==> than, that, the
data/hol-light-20190729/Examples/mccarthy.ml:104: intruction ==> instruction
data/hol-light-20190729/Examples/mizar.ml:118: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:119: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:121: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:122: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:130: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:131: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:133: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:134: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:135: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:136: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:138: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:139: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:141: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:142: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:145: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:147: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:152: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:152: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:155: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:156: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:158: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:181: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:182: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:211: wth ==> with
data/hol-light-20190729/Examples/mizar.ml:212: wth ==> with
data/hol-light-20190729/Examples/mizar.ml:235: wth ==> with
data/hol-light-20190729/Examples/mizar.ml:236: wth ==> with
data/hol-light-20190729/Examples/mizar.ml:518: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:519: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:523: ths ==> the, this
data/hol-light-20190729/Examples/mizar.ml:524: ths ==> the, this
data/hol-light-20190729/Examples/prover9.ml:349: ths ==> the, this
data/hol-light-20190729/Examples/prover9.ml:354: ths ==> the, this
data/hol-light-20190729/Examples/prover9.ml:397: ths ==> the, this
data/hol-light-20190729/Examples/prover9.ml:401: ths ==> the, this
data/hol-light-20190729/Examples/prover9.ml:402: ths ==> the, this
data/hol-light-20190729/Examples/prover9.ml:409: ths ==> the, this
data/hol-light-20190729/Examples/prover9.ml:410: ths ==> the, this
data/hol-light-20190729/Examples/prover9.ml:412: ths ==> the, this
data/hol-light-20190729/Examples/prover9.ml:423: ths ==> the, this
data/hol-light-20190729/Examples/prover9.ml:449: ths ==> the, this
data/hol-light-20190729/Examples/prover9.ml:476: ths ==> the, this
data/hol-light-20190729/Examples/prover9.ml:477: ths ==> the, this
data/hol-light-20190729/Examples/sos.ml:460: atleast ==> at least
data/hol-light-20190729/Examples/sos.ml:461: atleast ==> at least
data/hol-light-20190729/Examples/sos.ml:1321: ths ==> the, this
data/hol-light-20190729/Examples/sos.ml:1322: ths ==> the, this
data/hol-light-20190729/Examples/sos.ml:1329: ths ==> the, this
data/hol-light-20190729/Examples/sos.ml:1330: ths ==> the, this
data/hol-light-20190729/Examples/ste.ml:100: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:100: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:101: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:101: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:111: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:111: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:112: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:112: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:113: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:113: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:113: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:114: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:114: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:115: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:115: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:122: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:122: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:122: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:139: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:139: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:139: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:146: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:146: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:147: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:148: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:148: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:155: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:155: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:155: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:174: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:174: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:174: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:174: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:174: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:174: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:185: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:185: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:185: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:206: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:206: nd ==> and, 2nd
data/hol-light-20190729/Examples/ste.ml:206: nd ==> and, 2nd
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:920: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:921: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:992: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:996: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:1012: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:1016: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:1176: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:1178: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:1179: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:1188: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:1190: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:1240: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:1241: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:1244: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:1247: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:1326: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:1327: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:1327: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:1328: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:1331: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:1334: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:1344: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:1353: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:1378: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:1379: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:1422: larg ==> large
data/hol-light-20190729/Formal_ineqs/arith/arith_num.hl:1423: larg ==> large
data/hol-light-20190729/Formal_ineqs/lib/ssrbool.hl:61: isT ==> is, it, its, it's, sit, list
data/hol-light-20190729/Formal_ineqs/lib/ssrnat.hl:1800: halfS ==> halves
data/hol-light-20190729/Formal_ineqs/lib/ssrnat.hl:1801: halfS ==> halves
data/hol-light-20190729/Formal_ineqs/lib/ssrnat.hl:1819: halfS ==> halves
data/hol-light-20190729/Formal_ineqs/lib/ssrnat.hl:1819: halfS ==> halves
data/hol-light-20190729/Formal_ineqs/lib/ssrnat.hl:1836: halfS ==> halves
data/hol-light-20190729/Formal_ineqs/lib/ssrnat.hl:1836: halfS ==> halves
data/hol-light-20190729/Formal_ineqs/lib/ssrnat.hl:1844: halfS ==> halves
data/hol-light-20190729/Formal_ineqs/lib/ssrnat.hl:1844: halfS ==> halves
data/hol-light-20190729/Formal_ineqs/lib/ssrnat.hl:1853: halfS ==> halves
data/hol-light-20190729/Formal_ineqs/lib/ssrnat.hl:1853: halfS ==> halves
data/hol-light-20190729/Formal_ineqs/lib/ssrnat.hl:1862: halfS ==> halves
data/hol-light-20190729/Formal_ineqs/lib/ssrnat.hl:1862: halfS ==> halves
data/hol-light-20190729/Formal_ineqs/lib/ssrnat.hl:1870: halfS ==> halves
data/hol-light-20190729/Formal_ineqs/lib/ssrnat.hl:1870: halfS ==> halves
data/hol-light-20190729/Formal_ineqs/lib/ssrnat.hl:1885: halfS ==> halves
data/hol-light-20190729/Formal_ineqs/lib/ssrnat.hl:1885: halfS ==> halves
data/hol-light-20190729/Formal_ineqs/lib/ssreflect/ssreflect.hl:62: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/lib/ssreflect/ssreflect.hl:63: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/lib/ssreflect/ssreflect.hl:74: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/lib/ssreflect/ssreflect.hl:75: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/lib/ssreflect/ssreflect.hl:531: occurences ==> occurrences
data/hol-light-20190729/Formal_ineqs/lib/ssreflect/ssreflect.hl:1046: occurences ==> occurrences
data/hol-light-20190729/Formal_ineqs/misc/misc_functions.hl:13: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/misc/misc_functions.hl:13: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/taylor/m_taylor_arith.hl:145: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/taylor/m_taylor_arith.hl:146: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/taylor/m_taylor_arith.hl:147: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/taylor/m_taylor_arith.hl:168: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/taylor/m_taylor_arith.hl:185: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/taylor/m_taylor_arith.hl:186: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/taylor/m_taylor_arith.hl:187: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/taylor/m_taylor_arith.hl:187: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/taylor/m_taylor_arith.hl:188: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/taylor/m_taylor_arith.hl:190: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/taylor/m_taylor_arith.hl:210: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/taylor/m_taylor_arith.hl:211: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/taylor/m_taylor_arith.hl:212: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/taylor/m_taylor_arith.hl:224: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/taylor/m_taylor_arith.hl:225: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/taylor/m_taylor_arith.hl:226: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/taylor/theory/multivariate_taylor-compiled.hl:3307: te ==> the, be, we
data/hol-light-20190729/Formal_ineqs/taylor/theory/multivariate_taylor-compiled.hl:3334: te ==> the, be, we
data/hol-light-20190729/Formal_ineqs/taylor/theory/multivariate_taylor-compiled.hl:3336: te ==> the, be, we
data/hol-light-20190729/Formal_ineqs/taylor/theory/multivariate_taylor.vhl:2685: te ==> the, be, we
data/hol-light-20190729/Formal_ineqs/taylor/theory/multivariate_taylor.vhl:2712: te ==> the, be, we
data/hol-light-20190729/Formal_ineqs/taylor/theory/multivariate_taylor.vhl:2714: te ==> the, be, we
data/hol-light-20190729/Formal_ineqs/taylor/theory/taylor_interval-compiled.hl:1405: ba ==> by, be
data/hol-light-20190729/Formal_ineqs/taylor/theory/taylor_interval-compiled.hl:1406: ba ==> by, be
data/hol-light-20190729/Formal_ineqs/taylor/theory/taylor_interval-compiled.hl:1406: ba ==> by, be
data/hol-light-20190729/Formal_ineqs/taylor/theory/taylor_interval.vhl:1000: ba ==> by, be
data/hol-light-20190729/Formal_ineqs/taylor/theory/taylor_interval.vhl:1001: ba ==> by, be
data/hol-light-20190729/Formal_ineqs/verifier/m_verifier.hl:1232: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/verifier/m_verifier.hl:1233: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/verifier/m_verifier.hl:1233: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/verifier/m_verifier.hl:1251: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/verifier/m_verifier.hl:1253: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/verifier/m_verifier.hl:1260: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/verifier/m_verifier.hl:1261: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/verifier/m_verifier.hl:1261: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/verifier/m_verifier.hl:1436: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/verifier/m_verifier.hl:1438: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/verifier/m_verifier.hl:1445: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/verifier/m_verifier.hl:1446: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/verifier/m_verifier.hl:1446: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/verifier/m_verifier.hl:1613: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/verifier/m_verifier.hl:1615: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/verifier/m_verifier.hl:1622: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/verifier/m_verifier.hl:1623: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/verifier/m_verifier.hl:1623: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/verifier/m_verifier_main.hl:738: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/verifier/m_verifier_main.hl:739: ths ==> the, this
data/hol-light-20190729/Formal_ineqs/verifier/m_verifier_main.hl:740: ths ==> the, this
data/hol-light-20190729/Functionspaces/cfunspace.ml:603: ths ==> the, this
data/hol-light-20190729/Functionspaces/cfunspace.ml:606: ths ==> the, this
data/hol-light-20190729/Geometric_Algebra/geometricalgebra.ml:1611: ACI ==> ACPI
data/hol-light-20190729/Help/CACHE_CONV.doc:6: cacheing ==> caching
data/hol-light-20190729/Help/EVERY_TCL.doc:19: thn ==> then
data/hol-light-20190729/Help/GEN_SIMPLIFY_CONV.doc:9: strat ==> start, strata
data/hol-light-20190729/Help/GEN_SIMPLIFY_CONV.doc:11: strat ==> start, strata
data/hol-light-20190729/Help/HIGHER_REWRITE_CONV.doc:9: thn ==> then
data/hol-light-20190729/Help/HIGHER_REWRITE_CONV.doc:11: thn ==> then
data/hol-light-20190729/Help/HINT_EXISTS_TAC.doc:6: Attemps ==> Attempts
data/hol-light-20190729/Help/IMP_REWRITE_TAC.doc:14: instantations ==> instantiations
data/hol-light-20190729/Help/INTRO_TAC.doc:28: separed ==> separated
data/hol-light-20190729/Help/PROVE_HYP.doc:20: occurr ==> occur
data/hol-light-20190729/Help/PURE_SIMP_RULE.doc:11: Howver ==> However
data/hol-light-20190729/Help/RING_AND_IDEAL_CONV.doc:13: parms ==> params, prams
data/hol-light-20190729/Help/RING_AND_IDEAL_CONV.doc:17: parms ==> params, prams
data/hol-light-20190729/Help/RING_AND_IDEAL_CONV.doc:17: parms ==> params, prams
data/hol-light-20190729/Help/SUBS.doc:27: thn ==> then
data/hol-light-20190729/Help/SUBS_CONV.doc:11: thi ==> the, this
data/hol-light-20190729/Help/a.doc:25: atleast ==> at least
data/hol-light-20190729/Help/atleast.doc:1: atleast ==> at least
data/hol-light-20190729/Help/atleast.doc:3: atleast ==> at least
data/hol-light-20190729/Help/atleast.doc:9: atleast ==> at least
data/hol-light-20190729/Help/atleast.doc:14: atleast ==> at least
data/hol-light-20190729/Help/atleast.doc:26: atleast ==> at least
data/hol-light-20190729/Help/elistof.doc:30: atleast ==> at least
data/hol-light-20190729/Help/finished.doc:29: atleast ==> at least
data/hol-light-20190729/Help/fix.doc:27: atleast ==> at least
data/hol-light-20190729/Help/install_user_printer.doc:3: formater ==> formatter
data/hol-light-20190729/Help/leftbin.doc:38: atleast ==> at least
data/hol-light-20190729/Help/list_mk_gabs.doc:9: interated ==> iterated, interacted
data/hol-light-20190729/Help/listof.doc:29: atleast ==> at least
data/hol-light-20190729/Help/many.doc:27: atleast ==> at least
data/hol-light-20190729/Help/nothing.doc:29: atleast ==> at least
data/hol-light-20190729/Help/possibly.doc:26: atleast ==> at least
data/hol-light-20190729/Help/prove_general_recursive_function_exists.doc:51: upto ==> up to
data/hol-light-20190729/Help/prove_general_recursive_function_exists.doc:51: upto ==> up to
data/hol-light-20190729/Help/prove_general_recursive_function_exists.doc:54: upto ==> up to
data/hol-light-20190729/Help/prove_general_recursive_function_exists.doc:57: upto ==> up to
data/hol-light-20190729/Help/prove_general_recursive_function_exists.doc:58: upto ==> up to
data/hol-light-20190729/Help/prove_general_recursive_function_exists.doc:61: upto ==> up to
data/hol-light-20190729/Help/rightbin.doc:38: atleast ==> at least
data/hol-light-20190729/Help/some.doc:26: atleast ==> at least
data/hol-light-20190729/IEEE/ieee.hl:115: ans ==> and
data/hol-light-20190729/IEEE/ieee.hl:117: ans ==> and
data/hol-light-20190729/IEEE/ieee.hl:119: ans ==> and
data/hol-light-20190729/IEEE/ieee.hl:120: ans ==> and
data/hol-light-20190729/IEEE/ieee.hl:122: ans ==> and
data/hol-light-20190729/IEEE/ieee.hl:123: ans ==> and
data/hol-light-20190729/IEEE/ieee_thms.hl:336: ommitting ==> omitting
data/hol-light-20190729/IsabelleLight/README:90: allE ==> all, alley
data/hol-light-20190729/IsabelleLight/make.ml:21: allE ==> all, alley
data/hol-light-20190729/IsabelleLight/meta_rules.ml:252: allE ==> all, alley
data/hol-light-20190729/IsabelleLight/new_tactics.ml:103: allE ==> all, alley
data/hol-light-20190729/IsabelleLight/new_tactics.ml:151: Usefull ==> Useful
data/hol-light-20190729/IsabelleLight/new_tactics.ml:225: occured ==> occurred
data/hol-light-20190729/Jordan/jordan_curve_theorem.ml:14365: claus ==> clause
data/hol-light-20190729/Jordan/jordan_curve_theorem.ml:14556: claus ==> clause
data/hol-light-20190729/Jordan/jordan_curve_theorem.ml:14718: claus ==> clause
data/hol-light-20190729/Jordan/jordan_curve_theorem.ml:18385: ans ==> and
data/hol-light-20190729/Jordan/jordan_curve_theorem.ml:27813: 1nd ==> 1st
data/hol-light-20190729/Jordan/tactics_ext2.ml:194: Ambiguious ==> Ambiguous
data/hol-light-20190729/Jordan/tactics_ext2.ml:1326: assum ==> assume
data/hol-light-20190729/Jordan/tactics_ext2.ml:1330: assum ==> assume
data/hol-light-20190729/Jordan/tactics_ext2.ml:1384: assum ==> assume
data/hol-light-20190729/Jordan/tactics_ext2.ml:1388: assum ==> assume
data/hol-light-20190729/Library/analysis.ml:118: thi ==> the, this
data/hol-light-20190729/Library/analysis.ml:119: thi ==> the, this
data/hol-light-20190729/Library/analysis.ml:120: thi ==> the, this
data/hol-light-20190729/Library/analysis.ml:121: thi ==> the, this
data/hol-light-20190729/Library/analysis.ml:150: ths ==> the, this
data/hol-light-20190729/Library/analysis.ml:152: ths ==> the, this
data/hol-light-20190729/Library/analysis.ml:153: ths ==> the, this
data/hol-light-20190729/Library/analysis.ml:2609: dorder ==> order, disorder
data/hol-light-20190729/Library/analysis.ml:2632: dorder ==> order, disorder
data/hol-light-20190729/Library/analysis.ml:2636: dorder ==> order, disorder
data/hol-light-20190729/Library/analysis.ml:2659: dorder ==> order, disorder
data/hol-light-20190729/Library/analysis.ml:2670: dorder ==> order, disorder
data/hol-light-20190729/Library/analysis.ml:2680: dorder ==> order, disorder
data/hol-light-20190729/Library/analysis.ml:2681: dorder ==> order, disorder
data/hol-light-20190729/Library/analysis.ml:2729: dorder ==> order, disorder
data/hol-light-20190729/Library/analysis.ml:2925: dorder ==> order, disorder
data/hol-light-20190729/Library/analysis.ml:2943: dorder ==> order, disorder
data/hol-light-20190729/Library/analysis.ml:3007: dorder ==> order, disorder
data/hol-light-20190729/Library/analysis.ml:3020: dorder ==> order, disorder
data/hol-light-20190729/Library/analysis.ml:3031: dorder ==> order, disorder
data/hol-light-20190729/Library/analysis.ml:3044: dorder ==> order, disorder
data/hol-light-20190729/Library/analysis.ml:3072: dorder ==> order, disorder
data/hol-light-20190729/Library/analysis.ml:3137: dorder ==> order, disorder
data/hol-light-20190729/Library/analysis.ml:3164: dorder ==> order, disorder
data/hol-light-20190729/Library/analysis.ml:3186: dorder ==> order, disorder
data/hol-light-20190729/Library/calc_real.ml:1719: ths ==> the, this
data/hol-light-20190729/Library/calc_real.ml:1721: ths ==> the, this
data/hol-light-20190729/Library/calc_real.ml:1905: ths ==> the, this
data/hol-light-20190729/Library/calc_real.ml:1907: ths ==> the, this
data/hol-light-20190729/Library/calc_real.ml:2005: ths ==> the, this
data/hol-light-20190729/Library/calc_real.ml:2007: ths ==> the, this
data/hol-light-20190729/Library/pocklington.ml:1601: tha ==> than, that, the
data/hol-light-20190729/Library/pocklington.ml:1602: tha ==> than, that, the
data/hol-light-20190729/Library/pocklington.ml:1602: tha ==> than, that, the
data/hol-light-20190729/Library/pocklington.ml:1612: ths ==> the, this
data/hol-light-20190729/Library/pocklington.ml:1613: ths ==> the, this
data/hol-light-20190729/Library/pocklington.ml:1637: ths ==> the, this
data/hol-light-20190729/Library/pocklington.ml:1638: ths ==> the, this
data/hol-light-20190729/Library/pratt.ml:914: ths ==> the, this
data/hol-light-20190729/Library/pratt.ml:915: ths ==> the, this
data/hol-light-20190729/Library/pratt.ml:939: ths ==> the, this
data/hol-light-20190729/Library/pratt.ml:940: ths ==> the, this
data/hol-light-20190729/Library/q.ml:26: inferrable ==> inferable
data/hol-light-20190729/Library/transc.ml:1190: tha ==> than, that, the
data/hol-light-20190729/Library/transc.ml:1191: tha ==> than, that, the
data/hol-light-20190729/Library/transc.ml:3396: thi ==> the, this
data/hol-light-20190729/Library/transc.ml:3397: thi ==> the, this
data/hol-light-20190729/Library/transc.ml:3457: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4092: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4092: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4096: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4133: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4134: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4269: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4274: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4333: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4336: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4339: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4361: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4362: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4368: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4377: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4387: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4392: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4392: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4393: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4398: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4398: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4403: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4413: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4413: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4414: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4415: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4431: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4431: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4432: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4449: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4470: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4470: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4477: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4477: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4488: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4488: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4494: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4496: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4499: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4500: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4523: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4598: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4598: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4599: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4610: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4894: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4896: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4924: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4926: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4957: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4970: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4971: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4988: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:4989: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:5032: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:5073: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:5163: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:5203: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:5209: defint ==> definite, define
data/hol-light-20190729/Library/transc.ml:5304: defint ==> definite, define
data/hol-light-20190729/Logic/unif.ml:1409: ans ==> and
data/hol-light-20190729/Logic/unif.ml:1409: ans ==> and
data/hol-light-20190729/Logic/unif.ml:1410: ans ==> and
data/hol-light-20190729/Logic/unif.ml:1410: ans ==> and
data/hol-light-20190729/Logic/unif.ml:1413: ans ==> and
data/hol-light-20190729/Logic/unif.ml:1711: ans ==> and
data/hol-light-20190729/Logic/unif.ml:1712: ans ==> and
data/hol-light-20190729/Logic/unif.ml:1712: ans ==> and
data/hol-light-20190729/Logic/unif.ml:1713: ans ==> and
data/hol-light-20190729/Logic/unif.ml:1715: ans ==> and
data/hol-light-20190729/Logic/unif.ml:1733: ans ==> and
data/hol-light-20190729/Logic/unif.ml:1750: ans ==> and
data/hol-light-20190729/Logic/unif.ml:1751: ans ==> and
data/hol-light-20190729/Logic/unif.ml:1751: ans ==> and
data/hol-light-20190729/Logic/unif.ml:1752: ans ==> and
data/hol-light-20190729/Logic/unif.ml:1754: ans ==> and
data/hol-light-20190729/Minisat/dimacs_tools.ml:213: Refererence ==> Reference
data/hol-light-20190729/Minisat/minisat_parse.ml:16: lits ==> list
data/hol-light-20190729/Minisat/minisat_parse.ml:70: lits ==> list
data/hol-light-20190729/Minisat/minisat_parse.ml:90: lits ==> list
data/hol-light-20190729/Minisat/minisat_prove.ml:234: ths ==> the, this
data/hol-light-20190729/Minisat/minisat_prove.ml:237: ths ==> the, this
data/hol-light-20190729/Minisat/sat_tools.ml:63: alredy ==> already
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:102: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:104: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:110: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:124: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:134: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:135: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:135: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:136: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:136: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:136: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:136: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:136: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:137: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:138: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:138: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:143: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:144: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:144: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:145: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:146: Lits ==> List
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:147: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:147: Lits ==> List
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:149: Lits ==> List
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:150: Lits ==> List
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:391: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:394: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:395: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:397: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:399: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:413: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:415: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:417: lits ==> list
data/hol-light-20190729/Minisat/zc2mso/zc2mso.C:419: lits ==> list
data/hol-light-20190729/Mizarlight/duality_holby.ml:6: ths ==> the, this
data/hol-light-20190729/Mizarlight/duality_holby.ml:6: ths ==> the, this
data/hol-light-20190729/Model/syntax.ml:309: Substition ==> Substitution
data/hol-light-20190729/Multivariate/canal.ml:2422: ths ==> the, this
data/hol-light-20190729/Multivariate/canal.ml:2427: ths ==> the, this
data/hol-light-20190729/Multivariate/canal.ml:2450: ths ==> the, this
data/hol-light-20190729/Multivariate/canal.ml:2455: ths ==> the, this
data/hol-light-20190729/Multivariate/cauchy.ml:2565: ba ==> by, be
data/hol-light-20190729/Multivariate/complexes.ml:883: ths ==> the, this
data/hol-light-20190729/Multivariate/complexes.ml:884: ths ==> the, this
data/hol-light-20190729/Multivariate/complexes.ml:891: ths ==> the, this
data/hol-light-20190729/Multivariate/complexes.ml:892: ths ==> the, this
data/hol-light-20190729/Multivariate/convex.ml:13: miscelleneous ==> miscellaneous
data/hol-light-20190729/Multivariate/derivatives.ml:4428: continous ==> continuous
data/hol-light-20190729/Multivariate/determinants.ml:4244: ths ==> the, this
data/hol-light-20190729/Multivariate/determinants.ml:4248: ths ==> the, this
data/hol-light-20190729/Multivariate/determinants.ml:4248: ths ==> the, this
data/hol-light-20190729/Multivariate/determinants.ml:4249: ths ==> the, this
data/hol-light-20190729/Multivariate/determinants.ml:4268: ths ==> the, this
data/hol-light-20190729/Multivariate/determinants.ml:4269: ths ==> the, this
data/hol-light-20190729/Multivariate/determinants.ml:4269: ths ==> the, this
data/hol-light-20190729/Multivariate/determinants.ml:4322: ths ==> the, this
data/hol-light-20190729/Multivariate/determinants.ml:4325: ths ==> the, this
data/hol-light-20190729/Multivariate/determinants.ml:4334: ths ==> the, this
data/hol-light-20190729/Multivariate/determinants.ml:4337: ths ==> the, this
data/hol-light-20190729/Multivariate/determinants.ml:4438: thq ==> the
data/hol-light-20190729/Multivariate/determinants.ml:4440: thq ==> the
data/hol-light-20190729/Multivariate/determinants.ml:4441: thq ==> the
data/hol-light-20190729/Multivariate/flyspeck.ml:27: miscelleneous ==> miscellaneous
data/hol-light-20190729/Multivariate/gamma.ml:1551: Thw ==> The, thaw
data/hol-light-20190729/Multivariate/integration.ml:14892: ba ==> by, be
data/hol-light-20190729/Multivariate/integration.ml:14892: ba ==> by, be
data/hol-light-20190729/Multivariate/measure.ml:28443: miscellanous ==> miscellaneous
data/hol-light-20190729/Multivariate/metric.ml:4886: arbitarily ==> arbitrarily
data/hol-light-20190729/Multivariate/metric.ml:14071: Neigbourhood ==> Neighbourhood
data/hol-light-20190729/Multivariate/realanalysis.ml:4807: ba ==> by, be
data/hol-light-20190729/Multivariate/realanalysis.ml:14587: ths ==> the, this
data/hol-light-20190729/Multivariate/realanalysis.ml:14594: ths ==> the, this
data/hol-light-20190729/Multivariate/realanalysis.ml:14596: ths ==> the, this
data/hol-light-20190729/Multivariate/specialtopologies.ml:2: counterintuive ==> counter intuitive
data/hol-light-20190729/Multivariate/topology.ml:22771: vesion ==> version
data/hol-light-20190729/Multivariate/vectors.ml:940: ths ==> the, this
data/hol-light-20190729/Multivariate/vectors.ml:943: ths ==> the, this
data/hol-light-20190729/Multivariate/vectors.ml:970: ths ==> the, this
data/hol-light-20190729/Multivariate/vectors.ml:970: ths ==> the, this
data/hol-light-20190729/Multivariate/wlog.ml:361: thq ==> the
data/hol-light-20190729/Multivariate/wlog.ml:363: thq ==> the
data/hol-light-20190729/Multivariate/wlog.ml:364: thq ==> the
data/hol-light-20190729/Ntrie/ntrie.ml:145: conjuction ==> conjunction
data/hol-light-20190729/Ntrie/ntrie.ml:162: conjuction ==> conjunction
data/hol-light-20190729/Permutation/morelist.ml:194: forse ==> force
data/hol-light-20190729/Proofrecording/diffs/equal.ml:275: ths ==> the, this
data/hol-light-20190729/Proofrecording/diffs/equal.ml:276: ths ==> the, this
data/hol-light-20190729/Proofrecording/diffs/equal.ml:277: ths ==> the, this
data/hol-light-20190729/Proofrecording/diffs/equal.ml:283: ths ==> the, this
data/hol-light-20190729/Proofrecording/diffs/equal.ml:295: ths ==> the, this
data/hol-light-20190729/Proofrecording/diffs/equal.ml:295: ths ==> the, this
data/hol-light-20190729/Proofrecording/diffs/proofobjects_coq.ml:162: improvment ==> improvement
data/hol-light-20190729/Proofrecording/diffs/proofobjects_coq.ml:184: improvment ==> improvement
data/hol-light-20190729/Proofrecording/diffs/proofobjects_coq.ml:237: improvment ==> improvement
data/hol-light-20190729/Proofrecording/diffs/proofobjects_coq.ml:1398: te ==> the, be, we
data/hol-light-20190729/Proofrecording/diffs/proofobjects_coq.ml:1400: te ==> the, be, we
data/hol-light-20190729/Proofrecording/diffs/tactics.ml:113: ths ==> the, this
data/hol-light-20190729/Proofrecording/diffs/tactics.ml:114: ths ==> the, this
data/hol-light-20190729/Proofrecording/diffs/tactics.ml:128: ths ==> the, this
data/hol-light-20190729/Proofrecording/diffs/tactics.ml:129: ths ==> the, this
data/hol-light-20190729/Proofrecording/diffs/tactics.ml:140: ths ==> the, this
data/hol-light-20190729/Proofrecording/diffs/tactics.ml:141: ths ==> the, this
data/hol-light-20190729/Proofrecording/diffs/tactics.ml:295: ths ==> the, this
data/hol-light-20190729/Proofrecording/diffs/tactics.ml:295: ths ==> the, this
data/hol-light-20190729/Proofrecording/diffs/tactics.ml:560: ths ==> the, this
data/hol-light-20190729/Proofrecording/diffs/tactics.ml:562: ths ==> the, this
data/hol-light-20190729/Proofrecording/diffs/tactics.ml:754: ths ==> the, this
data/hol-light-20190729/Proofrecording/diffs/tactics.ml:756: ths ==> the, this
data/hol-light-20190729/Proofrecording/diffs/tactics.ml:768: ths ==> the, this
data/hol-light-20190729/Proofrecording/diffs/tactics.ml:769: ths ==> the, this
data/hol-light-20190729/Proofrecording/diffs/tactics.ml:769: ths ==> the, this
data/hol-light-20190729/Proofrecording/diffs/tactics.ml:774: ths ==> the, this
data/hol-light-20190729/Proofrecording/diffs/tactics.ml:775: ths ==> the, this
data/hol-light-20190729/Proofrecording/diffs/tactics.ml:775: ths ==> the, this
data/hol-light-20190729/QBF/qbf.ml:675: conjuction ==> conjunction
data/hol-light-20190729/QBF/qbf.ml:712: conjuction ==> conjunction
data/hol-light-20190729/QBF/qbf.ml:720: conjuction ==> conjunction
data/hol-light-20190729/QBF/qbf.ml:722: conjuction ==> conjunction
data/hol-light-20190729/Quaternions/qcalc.hl:151: wth ==> with
data/hol-light-20190729/Quaternions/qcalc.hl:154: wth ==> with
data/hol-light-20190729/Quaternions/qcalc.hl:157: wth ==> with
data/hol-light-20190729/RichterHilbertAxiomGeometry/TarskiAxiomGeometry_read.ml:8: Methoden ==> Methods
data/hol-light-20190729/RichterHilbertAxiomGeometry/TarskiAxiomGeometry_read.ml:9: Geometrie ==> Geometry
data/hol-light-20190729/RichterHilbertAxiomGeometry/Topology.ml:128: OpenIn ==> opening
data/hol-light-20190729/RichterHilbertAxiomGeometry/Topology.ml:136: OpenIn ==> opening
data/hol-light-20190729/RichterHilbertAxiomGeometry/Topology.ml:373: OpenIn ==> opening
data/hol-light-20190729/RichterHilbertAxiomGeometry/error-checking.ml:141: prooof ==> proof
data/hol-light-20190729/RichterHilbertAxiomGeometry/error-checking.ml:153: prooof ==> proof
data/hol-light-20190729/RichterHilbertAxiomGeometry/from_topology.ml:14787: vesion ==> version
data/hol-light-20190729/RichterHilbertAxiomGeometry/from_topology.ml:17918: propery ==> property, properly
data/hol-light-20190729/RichterHilbertAxiomGeometry/readable.ml:275: ths ==> the, this
data/hol-light-20190729/RichterHilbertAxiomGeometry/readable.ml:275: ths ==> the, this
data/hol-light-20190729/RichterHilbertAxiomGeometry/thmTopology:168: OpenIn ==> opening
data/hol-light-20190729/RichterHilbertAxiomGeometry/miz3/Miz3Tips:208: intead ==> instead
data/hol-light-20190729/RichterHilbertAxiomGeometry/miz3/Miz3Tips:368: evaluting ==> evaluating
data/hol-light-20190729/Rqe/defs.ml:24: Intepretation ==> Interpretation
data/hol-light-20190729/Rqe/examples.ml:671: Loos ==> Loose, lose
data/hol-light-20190729/Rqe/inferpsign.ml:39: aks ==> ask
data/hol-light-20190729/Rqe/inferpsign.ml:40: aks ==> ask
data/hol-light-20190729/Rqe/inferpsign.ml:169: asign ==> assign
data/hol-light-20190729/Rqe/inferpsign.ml:215: asign ==> assign
data/hol-light-20190729/Rqe/inferpsign.ml:216: asign ==> assign
data/hol-light-20190729/Rqe/inferpsign.ml:276: asign ==> assign
data/hol-light-20190729/Rqe/inferpsign.ml:277: asign ==> assign
data/hol-light-20190729/Rqe/lift_qelim.ml:2: ths ==> the, this
data/hol-light-20190729/Rqe/lift_qelim.ml:4: ths ==> the, this
data/hol-light-20190729/Rqe/lift_qelim.ml:4: ths ==> the, this
data/hol-light-20190729/Rqe/lift_qelim.ml:5: ths ==> the, this
data/hol-light-20190729/Rqe/rqe_tactics_ext.ml:200: assum ==> assume
data/hol-light-20190729/Rqe/rqe_tactics_ext.ml:201: assum ==> assume
data/hol-light-20190729/Rqe/util.ml:44: assum ==> assume
data/hol-light-20190729/Tutorial/Changing_proof_style.ml:31: ths ==> the, this
data/hol-light-20190729/Tutorial/Changing_proof_style.ml:31: ths ==> the, this
data/hol-light-20190729/Tutorial/Custom_inference_rules.ml:73: ths ==> the, this
data/hol-light-20190729/Tutorial/Custom_inference_rules.ml:73: ths ==> the, this
data/hol-light-20190729/Tutorial/Custom_inference_rules.ml:95: tha ==> than, that, the
data/hol-light-20190729/Tutorial/Custom_inference_rules.ml:96: tha ==> than, that, the
data/hol-light-20190729/Tutorial/HOL_as_a_functional_programming_language.ml:59: ths ==> the, this
data/hol-light-20190729/Tutorial/HOL_as_a_functional_programming_language.ml:59: ths ==> the, this
data/hol-light-20190729/Tutorial/Linking_external_tools.ml:145: defint ==> definite, define
data/hol-light-20190729/Tutorial/all.ml:418: ths ==> the, this
data/hol-light-20190729/Tutorial/all.ml:418: ths ==> the, this
data/hol-light-20190729/Tutorial/all.ml:1408: ths ==> the, this
data/hol-light-20190729/Tutorial/all.ml:1408: ths ==> the, this
data/hol-light-20190729/Tutorial/all.ml:1977: ths ==> the, this
data/hol-light-20190729/Tutorial/all.ml:1977: ths ==> the, this
data/hol-light-20190729/Tutorial/all.ml:1999: tha ==> than, that, the
data/hol-light-20190729/Tutorial/all.ml:2000: tha ==> than, that, the
data/hol-light-20190729/Tutorial/all.ml:2228: defint ==> definite, define
data/hol-light-20190729/Unity/aux_definitions.ml:18: Auxilliary ==> Auxiliary
data/hol-light-20190729/Unity/mk_comp_unity.ml:22: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:23: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:23: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:27: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:28: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:28: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:48: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:49: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:49: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:53: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:54: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:54: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:74: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:75: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:75: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:79: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:80: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:80: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:89: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:90: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:90: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:91: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:95: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:96: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:96: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:139: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:140: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:141: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:141: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:145: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:146: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:147: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:148: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:172: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:173: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:173: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:174: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:178: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:179: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:180: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:181: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:189: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:190: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:190: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:194: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:195: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:196: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:205: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:206: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:206: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:210: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:211: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:212: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:221: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:222: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:223: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:227: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:228: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:229: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:237: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:238: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:238: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:242: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:243: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:243: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:249: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:250: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:250: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:254: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:255: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:255: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:281: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:282: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:283: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:287: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:288: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:289: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:302: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:303: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:303: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:307: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:308: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:308: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:339: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:339: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:343: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:343: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:349: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:349: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:349: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:353: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:353: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:359: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:359: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:359: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:363: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:363: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:369: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:370: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:370: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:374: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:375: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:375: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:388: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:389: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:389: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:393: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:394: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:394: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:423: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:424: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:424: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:428: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:429: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:429: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:438: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:439: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:439: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:443: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:444: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:444: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:451: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:452: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:452: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:522: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:522: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:522: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:526: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:527: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:527: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:537: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:538: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:538: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:542: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:543: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_comp_unity.ml:545: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_ensures.ml:22: existance ==> existence
data/hol-light-20190729/Unity/mk_ensures.ml:256: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_ensures.ml:257: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_ensures.ml:258: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_ensures.ml:269: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_ensures.ml:270: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_ensures.ml:271: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_ensures.ml:291: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_ensures.ml:292: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_ensures.ml:293: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_ensures.ml:343: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_ensures.ml:344: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_ensures.ml:345: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_ensures.ml:362: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_ensures.ml:363: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_ensures.ml:364: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_ensures.ml:381: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_ensures.ml:382: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_ensures.ml:383: FPr ==> for, far, fps
data/hol-light-20190729/Unity/mk_leadsto.ml:1878: litte ==> little
data/hol-light-20190729/Unity/mk_leadsto.ml:3366: propertie ==> property, properties
data/hol-light-20190729/Unity/mk_unity_prog.ml:133: funtion ==> function
data/hol-light-20190729/Unity/mk_unity_prog.ml:159: otherwize ==> otherwise
data/hol-light-20190729/Unity/mk_unity_prog.ml:195: exisiting ==> existing
data/hol-light-20190729/Unity/mk_unity_prog.ml:201: representaion ==> representation
data/hol-light-20190729/Unity/mk_unity_prog.ml:213: funtion ==> function
data/hol-light-20190729/Unity/mk_unless.ml:26: tripple ==> triple
data/hol-light-20190729/miz3/miz3.ml:94: atleast ==> at least
data/hol-light-20190729/miz3/miz3.ml:277: ths ==> the, this
data/hol-light-20190729/miz3/miz3.ml:278: ths ==> the, this
data/hol-light-20190729/miz3/miz3.ml:281: ths ==> the, this
data/hol-light-20190729/miz3/miz3.ml:281: ths ==> the, this
data/hol-light-20190729/miz3/miz3.ml:596: justs ==> just
data/hol-light-20190729/miz3/miz3.ml:598: justs ==> just
data/hol-light-20190729/miz3/miz3.ml:1106: ths ==> the, this
data/hol-light-20190729/miz3/miz3.ml:1106: ths ==> the, this
data/hol-light-20190729/miz3/miz3.ml:1122: ths ==> the, this
data/hol-light-20190729/miz3/miz3.ml:1123: ths ==> the, this
data/hol-light-20190729/miz3/miz3.ml:1135: ths ==> the, this
data/hol-light-20190729/miz3/miz3.ml:1136: ths ==> the, this
data/hol-light-20190729/miz3/miz3.ml:1272: ths ==> the, this
data/hol-light-20190729/miz3/miz3.ml:1273: ths ==> the, this
data/hol-light-20190729/miz3/miz3.ml:1273: ths ==> the, this
data/hol-light-20190729/miz3/miz3.ml:1386: ths ==> the, this
data/hol-light-20190729/miz3/miz3.ml:1386: ths ==> the, this
data/hol-light-20190729/debian/changelog:32: udpate ==> update
data/hol-light-20190729/.pc/cd-holtest-parallel.patch/holtest_parallel:38: follwing ==> following
data/hol-light-20190729/.pc/0004-Fix-compilation-with-camlp5-7.11.patch/pa_j_4.xx_7.xx.ml:378: ExTry ==> entry
data/hol-light-20190729/.pc/0004-Fix-compilation-with-camlp5-7.11.patch/pa_j_4.xx_7.xx.ml:380: ExTry ==> entry
data/hol-light-20190729/.pc/0004-Fix-compilation-with-camlp5-7.11.patch/pa_j_4.xx_7.xx.ml:1644: upto ==> up to
data/hol-light-20190729/.pc/0004-Fix-compilation-with-camlp5-7.11.patch/pa_j_4.xx_7.xx.ml:2952: upto ==> up to
data/hol-light-20190729/.pc/0004-Fix-compilation-with-camlp5-7.11.patch/pa_j_4.xx_7.xx.ml:2952: upto ==> up to