src/HOL/HOL.thy
changeset 22270 4ccb7e6be929
parent 22218 30a8890d2967
child 22377 61610b1beedf