File Name.ML

open Name;

qed_goal "xn_cases" thy "\<forall>xn. xn = Throwable \<or> \
\          xn = NullPointer \<or> xn = OutOfMemory \<or> xn = ClassCast \<or> \
\          xn = NegArrSize  \<or> xn = IndOutBound \<or> xn = ArrStore" (K [
	rtac allI 1,
	induct_tac "xn" 1,
	ALLGOALS Simp_tac]);