src/HOL/ex/Hilbert_Classical.thy
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2001-09-28 wenzelm 2001-09-28 tuned;
2001-09-27 wenzelm 2001-09-27 tuned;
2001-09-27 wenzelm 2001-09-27 tuned;
2001-09-27 wenzelm 2001-09-27 derive tertium-non-datur by means of Hilbert's choice operator;