HomeIsabelle/Phabricator

added lemmas multp_implies_one_step, one_step_implies_multp, and…

Description

added lemmas multp_implies_one_step, one_step_implies_multp, and subset_implies_multp

Details

Provenance
desharnaAuthored on
Parents
rISABELLE3e55e47a37e7: added lemma wfP_multp
Branches
Unknown
Tags
Unknown