src/HOL/ex/Classical.thy
changeset 14456 cca28ec5f9a6
parent 14249 05382e257d95
child 15008 5abd18710a1f