HOL

HOL copied to clipboard

FMA error in floating-point (?)

16

See, this from the Isabelle mailing list > It is possible that this formalisation is not faithful to the IEEE standard. The commit message of the changeset that is to...

mn200

Creating a conversion of indefinite integrals (antiderivatives) of real functions

2

Following some recent discussions on Slack, I'm considering writing a HOL conversion for computing indefinite integrals (antiderivatives) of real functions, which may be called `INTEGRATE_CONV`. After some investigations on the...

binghe

Congruence rule in TFL depends on bound variable

3

In the following, `valueOf` extracts a value from a monad (`'a M -> 'a`). This is possible, for example, in a writer monad. In something like the option monad, you'd...

mn200

Fixed OpenTheory build issues (#1045) introduced in #1043

5

Hi, this PR fixes the OpenTheory build issues described in #1045, i.e. a lot of leaking assumptions when installing `hol-real`. As I mentioned in #1045, these issues were introduced when...

binghe

OpenTheory issues after moving some definitions and theorems into realaxTheory

4

Hi, I'm sorry to report that, the OpenTheory packages (in particular, `hol-real`) built after #1043 (the new `REAL_ARITH_TAC`) now have a lot of leaking assumptions not covered by OpenTheory base...

binghe

In things like `cardeq_TRANS`, there's an extra type variable that gets turned into an ugly genvarified blob when you use `irule` or `irule_at`. Often, the desired type is clear; there...

mn200

Changes in COND_ELIM_CONV and SUB_AND_COND_ELIM_CONV

6

Hi, I occasionally found that the outputs of two COND-elimination conversions `COND_ELIM_CONV` and `SUB_AND_COND_ELIM_CONV` have changed w.r.t. their documentation, for instance: ``` > COND_ELIM_CONV ``!f n. f (if (SUC n...

binghe

Remaining issues of HOL's OpenTheory packaging

2

Following PR #803, I found the following remaining issues in OpenTheory packaging: 1. The recently added `itself` type in `boolTheory` introduced some new type, constant and theorems. When these theorems...

binghe

DO NOT merge yet! Attempt at unifying type abbreviations disabling mechanism in terms and type. Similar to the already existing `-tm` the syntax is `-:ty`. The previous type abbreviation disabling...

dwRchyngqxs

This issue is about implementing a version of `Q.REFINE_EXISTS_TAC` called `qrefinel : term quotation list -> tactic`, which: - Attempts to refine a goal consisting of nested top-level existentials with...

hrutvik