HomeIsabelle/Phabricator

use abs(h l - h r) instead of 3 cases, tuned proofs

Description

use abs(h l - h r) instead of 3 cases, tuned proofs

Details

Provenance
nipkowAuthored on
Parents
rISABELLE62b17adad0cc: added lemmas
Branches
Unknown
Tags
Unknown