src/HOL/HOL.thy
changeset 22337 d4599c206446
parent 22218 30a8890d2967
child 22377 61610b1beedf