src/HOL/HOL.thy
changeset 4176 84a0bfbd74e5
parent 4083 bcff38832d89
child 4371 8755cdbbf6b3