src/HOL/ex/Classical.thy
changeset 24505 9e6d91f8bb73
parent 24300 e170cee91c66
child 30607 c3d1590debd8