equal
deleted
inserted
replaced
1 (* Title: HOL/MicroJava/J/Conform.thy |
1 (* Title: HOL/MicroJava/J/Conform.thy |
2 Author: David von Oheimb |
2 Author: David von Oheimb |
3 Copyright 1999 Technische Universitaet Muenchen |
3 Copyright 1999 Technische Universitaet Muenchen |
4 *) |
4 *) |
5 |
5 |
6 section {* Conformity Relations for Type Soundness Proof *} |
6 section \<open>Conformity Relations for Type Soundness Proof\<close> |
7 |
7 |
8 theory Conform imports State WellType Exceptions begin |
8 theory Conform imports State WellType Exceptions begin |
9 |
9 |
10 type_synonym 'c env' = "'c prog \<times> (vname \<rightharpoonup> ty)" -- "same as @{text env} of @{text WellType.thy}" |
10 type_synonym 'c env' = "'c prog \<times> (vname \<rightharpoonup> ty)" -- "same as @{text env} of @{text WellType.thy}" |
11 |
11 |