author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45231  d85a2fdc586c 
child 58886  8a6cac7c7247 
permissions  rwrr 
12951  1 
(* Title: HOL/MicroJava/J/SystemClasses.thy 
2 
Author: Gerwin Klein 

3 
Copyright 2002 Technische Universitaet Muenchen 

4 
*) 

5 

6 
header {* \isaheader{System Classes} *} 

7 

16417  8 
theory SystemClasses imports Decl begin 
12951  9 

10 
text {* 

11 
This theory provides definitions for the @{text Object} class, 

12 
and the system exceptions. 

13 
*} 

14 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
28524
diff
changeset

15 
definition ObjectC :: "'c cdecl" where 
45231
d85a2fdc586c
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
bulwahn
parents:
44035
diff
changeset

16 
[code_unfold]: "ObjectC \<equiv> (Object, (undefined,[],[]))" 
12951  17 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
28524
diff
changeset

18 
definition NullPointerC :: "'c cdecl" where 
45231
d85a2fdc586c
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
bulwahn
parents:
44035
diff
changeset

19 
[code_unfold]: "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))" 
12951  20 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
28524
diff
changeset

21 
definition ClassCastC :: "'c cdecl" where 
45231
d85a2fdc586c
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
bulwahn
parents:
44035
diff
changeset

22 
[code_unfold]: "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))" 
12951  23 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
28524
diff
changeset

24 
definition OutOfMemoryC :: "'c cdecl" where 
45231
d85a2fdc586c
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
bulwahn
parents:
44035
diff
changeset

25 
[code_unfold]: "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))" 
12951  26 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
28524
diff
changeset

27 
definition SystemClasses :: "'c cdecl list" where 
45231
d85a2fdc586c
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
bulwahn
parents:
44035
diff
changeset

28 
[code_unfold]: "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]" 
12951  29 

30 
end 