equal
deleted
inserted
replaced
4 Copyright 1999 Technische Universitaet Muenchen |
4 Copyright 1999 Technische Universitaet Muenchen |
5 *) |
5 *) |
6 |
6 |
7 header {* \isaheader{Conformity Relations for Type Soundness Proof} *} |
7 header {* \isaheader{Conformity Relations for Type Soundness Proof} *} |
8 |
8 |
9 theory Conform = State + WellType + Exceptions: |
9 theory Conform imports State WellType Exceptions begin |
10 |
10 |
11 types 'c env_ = "'c prog \<times> (vname \<rightharpoonup> ty)" -- "same as @{text env} of @{text WellType.thy}" |
11 types 'c env_ = "'c prog \<times> (vname \<rightharpoonup> ty)" -- "same as @{text env} of @{text WellType.thy}" |
12 |
12 |
13 constdefs |
13 constdefs |
14 |
14 |