HomeIsabelle/Phabricator

explicit predicate for confined bit range avoids cyclic rewriting in presence…

Description

explicit predicate for confined bit range avoids cyclic rewriting in presence of extensionality rule for bit values (contributed by Thomas Sewell)

Details

Provenance
florian.haftmannAuthored on
Parents
rISABELLE7466b2a3905a: more latex macros;
Branches
Unknown
Tags
Unknown