equal
deleted
inserted
replaced
383 |
383 |
384 lemma ObjectC_neq_SXcptC [simp]: "ObjectC \<noteq> SXcptC xn" |
384 lemma ObjectC_neq_SXcptC [simp]: "ObjectC \<noteq> SXcptC xn" |
385 by (simp add: ObjectC_def SXcptC_def Object_def SXcpt_def) |
385 by (simp add: ObjectC_def SXcptC_def Object_def SXcpt_def) |
386 |
386 |
387 lemma SXcptC_inject [simp]: "(SXcptC xn = SXcptC xm) = (xn = xm)" |
387 lemma SXcptC_inject [simp]: "(SXcptC xn = SXcptC xm) = (xn = xm)" |
388 apply (simp add: SXcptC_def) |
388 by (simp add: SXcptC_def) |
389 apply auto |
|
390 done |
|
391 |
389 |
392 constdefs standard_classes :: "cdecl list" |
390 constdefs standard_classes :: "cdecl list" |
393 "standard_classes \<equiv> [ObjectC, SXcptC Throwable, |
391 "standard_classes \<equiv> [ObjectC, SXcptC Throwable, |
394 SXcptC NullPointer, SXcptC OutOfMemory, SXcptC ClassCast, |
392 SXcptC NullPointer, SXcptC OutOfMemory, SXcptC ClassCast, |
395 SXcptC NegArrSize , SXcptC IndOutBound, SXcptC ArrStore]" |
393 SXcptC NegArrSize , SXcptC IndOutBound, SXcptC ArrStore]" |