src/HOL/ex/Intuitionistic.thy
changeset 30458 804de935c328
parent 17589 58eeffd73be1
child 41460 ea56b98aee83