HomeIsabelle/Phabricator

put back Nat.le_diff_conv2 because AUTO2 doesn't work with Groups.le_diff_conv2

Description

put back Nat.le_diff_conv2 because AUTO2 doesn't work with Groups.le_diff_conv2

Details

Provenance
paulson <lp15@cam.ac.uk>Authored on
Parents
rISABELLE3904cfde1aa9: merged
Branches
Unknown
Tags
Unknown