equal
deleted
inserted
replaced
4 Copyright 1999 Technische Universitaet Muenchen |
4 Copyright 1999 Technische Universitaet Muenchen |
5 *) |
5 *) |
6 |
6 |
7 header {* \isaheader{Type Safety Proof} *} |
7 header {* \isaheader{Type Safety Proof} *} |
8 |
8 |
9 theory JTypeSafe = Eval + Conform: |
9 theory JTypeSafe imports Eval Conform begin |
10 |
10 |
11 declare split_beta [simp] |
11 declare split_beta [simp] |
12 |
12 |
13 lemma NewC_conforms: |
13 lemma NewC_conforms: |
14 "[|h a = None; (x,(h, l))::\<preceq>(G, lT); wf_prog wf_mb G; is_class G C|] ==> |
14 "[|h a = None; (x,(h, l))::\<preceq>(G, lT); wf_prog wf_mb G; is_class G C|] ==> |