diff -r 4f9803829625 -r 564ea783ace8 src/HOL/Parity.thy --- a/src/HOL/Parity.thy Wed Jan 21 18:37:44 2009 +0100 +++ b/src/HOL/Parity.thy Wed Jan 21 23:40:23 2009 +0100 @@ -8,7 +8,7 @@ imports Plain Presburger begin -class even_odd = type + +class even_odd = fixes even :: "'a \ bool" abbreviation