src/HOL/HOL.thy
changeset 17421 0382f6877b98
parent 17404 d16c3a62c396
child 17459 9a3925c07392