moved addsplits [expand_if] from HOL_basic_ss to HOL_ss;
(* Title: ZF/Cardinal_AC.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of CambridgeCardinal Arithmetic WITH the Axiom of Choice*)Cardinal_AC = CardinalArith + Zorn