1 Arith = FOL +
2 classes arith < term
3 consts "0" :: "'a::arith" ("0")
4 "1" :: "'a::arith" ("1")
5 "+" :: "['a::arith,'a] => 'a" (infixl 60)
6 end