src/HOL/HOL.thy
changeset 14456 cca28ec5f9a6
parent 14444 24724afce166
child 14565 c6dc17aab88a