Add ltree_every and ltree_finite_branching#1172

Merged

mn200 merged 3 commits intoHOL-Theorem-Prover:developfrom binghe:ltree_every_n_finite_branching

Dec 11, 2023

+81

Commits on Dec 11, 2023

[ltree] add ltree_every and ltree_finite_branching
binghe
committed
[ltree] add ltree_every_rewrite[simp] and ltree_finite_branching_rewrite[simp]
binghe
committed
Remove unnecessary GEN_REWRITE_TACs... (SimpLHS is also unnecessary)
binghe
committed