src/HOL/ex/Intuitionistic.thy
changeset 12791 ccc0f45ad2c4
parent 12450 1162b280700a
child 16417 9bc16273c2d4