equal
deleted
inserted
replaced
7 imports DefiniteAssignmentCorrect Conform |
7 imports DefiniteAssignmentCorrect Conform |
8 begin |
8 begin |
9 |
9 |
10 section "error free" |
10 section "error free" |
11 |
11 |
12 hide const field |
12 hide_const field |
13 |
13 |
14 lemma error_free_halloc: |
14 lemma error_free_halloc: |
15 assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and |
15 assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and |
16 error_free_s0: "error_free s0" |
16 error_free_s0: "error_free s0" |
17 shows "error_free s1" |
17 shows "error_free s1" |