--- a/src/FOL/FOL.thy Fri Feb 18 16:36:42 2011 +0100 +++ b/src/FOL/FOL.thy Fri Feb 18 17:03:30 2011 +0100 @@ -18,7 +18,7 @@ subsection {* The classical axiom *} -axioms +axiomatization where classical: "(~P ==> P) ==> P"