equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: David von Oheimb and Norbert Schirmer |
3 Author: David von Oheimb and Norbert Schirmer |
4 *) |
4 *) |
5 header {* The type soundness proof for Java *} |
5 header {* The type soundness proof for Java *} |
6 |
6 |
7 theory TypeSafe = DefiniteAssignmentCorrect + Conform: |
7 theory TypeSafe imports DefiniteAssignmentCorrect Conform begin |
8 |
8 |
9 section "error free" |
9 section "error free" |
10 |
10 |
11 lemma error_free_halloc: |
11 lemma error_free_halloc: |
12 assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and |
12 assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and |