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
rAFPa168f8f2bbc3: tuned signature, according to Isabelle/28a582aa25dd;
Branches
Unknown
Tags
Unknown