equal
deleted
inserted
replaced
6 section \<open>System Classes\<close> |
6 section \<open>System Classes\<close> |
7 |
7 |
8 theory SystemClasses imports Decl begin |
8 theory SystemClasses imports Decl begin |
9 |
9 |
10 text \<open> |
10 text \<open> |
11 This theory provides definitions for the @{text Object} class, |
11 This theory provides definitions for the \<open>Object\<close> class, |
12 and the system exceptions. |
12 and the system exceptions. |
13 \<close> |
13 \<close> |
14 |
14 |
15 definition ObjectC :: "'c cdecl" where |
15 definition ObjectC :: "'c cdecl" where |
16 [code_unfold]: "ObjectC \<equiv> (Object, (undefined,[],[]))" |
16 [code_unfold]: "ObjectC \<equiv> (Object, (undefined,[],[]))" |