Irvin

REABBREV_TAC renames duplicate abbreviations

3

Given a goal of ``` 0. Abbrev (a = FOO BAR) 1. Abbrev (a = GOO BAR) ------------------------------------ test ``` REABBREV_TAC results in this ``` 0. Abbrev (a = GOO...

Its really annoying to have to manually send regions with loads

Given a assumption of `foo :- (A /\ B)` a goal of A /\ B fs[L"foo"] should be simplified see zulip [#❄️ HOL4 > Label of conjuncts should be split.](https://hol.zulipchat.com/#narrow/channel/486798-.E2.9D.84.EF.B8.8F-HOL4/topic/Label.20of.20conjuncts.20should.20be.20split.2E/with/512447381)

See title. Work would consist of 1. making cong a separate attribute. Its currently a alias to defncong. 2. Figuring out how to make whatever that generates defncong thms also...

while Cases_on works on terms like `evaluate (xs,env,s)`, PairCases_on does not work.

Currently there's no easy way to identity theorems. This proposal would consist of warning when proving a theorem if a duplicate theorem already exists. There's a related zulip discussion. [#❄️...

irule_at any should work on universally quantifier conjuncts.

1

See zulip discussion [#❄️ HOL4 > Why does irule_at Any Fail](https://hol.zulipchat.com/#narrow/channel/486798-.E2.9D.84.EF.B8.8F-HOL4/topic/Why.20does.20irule_at.20Any.20Fail/with/504985160)

``` Theorem let_elim_repro: let x = y z q in A x /\ B x Proof LET_ELIM_TAC ``` In here LET_ELIM_TAC splits the goal into two subgoals ``` 2 subgoals:...

Refactor to use extended numerals.

1

Cakeml currently uses `num option` in various places where an extended numeral is more appropriate. for example in wordlang stack_size is a num option where NONE means the stack is...

This is about adding support for OS.Process.system to CakeML. Note that this issue includes adding models such that one can reason about sub processes.