src/HOL/Induct/ABexp.thy
changeset 75444 331f96a67924
parent 67443 3abf6a722518
equal deleted inserted replaced
75443:d6f2fbdc6322 75444:331f96a67924