src/HOL/IMP/Natural.thy
changeset 9789 7e5e6c47c0b5
parent 9241 f961c1fdff50
child 12431 07ec657249e5
equal deleted inserted replaced
9788:df671fa2562a 9789:7e5e6c47c0b5