src/HOL/Induct/ABexp.thy
changeset 79733 3e30ca77ccfe
parent 67443 3abf6a722518