equal
deleted
inserted
replaced
1 (* Title: HOL/MicroJava/Comp/CorrCompTp.thy |
1 (* Title: HOL/MicroJava/Comp/CorrCompTp.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Martin Strecker |
3 Author: Martin Strecker |
4 *) |
4 *) |
5 |
5 |
6 theory CorrCompTp = LemmasComp + JVM + TypeInf + Altern: |
6 theory CorrCompTp |
|
7 imports LemmasComp TypeInf "../BV/JVM" "../BV/Altern" |
|
8 begin |
7 |
9 |
8 declare split_paired_All [simp del] |
10 declare split_paired_All [simp del] |
9 declare split_paired_Ex [simp del] |
11 declare split_paired_Ex [simp del] |
10 |
12 |
11 |
13 |