src/HOL/Library/EfficientNat.thy
changeset 23315 df3a7e9ebadb
parent 23269 851b8ea067ac
child 23365 f31794033ae1