eliminated obsolete case_split_thm -- use case_split;
added case_split_tac (works without context);
setup for induct_tacs.ML;
Arith = FOL +
classes arith < term
consts "0" :: "'a::arith" ("0")
"1" :: "'a::arith" ("1")
"+" :: "['a::arith,'a] => 'a" (infixl 60)
end