| changeset 61361 | 8b5f00202e1a |
| parent 58886 | 8a6cac7c7247 |
| child 63258 | 576fb8068ba6 |
| 61360:a273bdac0934 | 61361:8b5f00202e1a |
|---|---|
1 (* Title: HOL/MicroJava/BV/EffectMono.thy |
1 (* Title: HOL/MicroJava/BV/EffectMono.thy |
2 Author: Gerwin Klein |
2 Author: Gerwin Klein |
3 Copyright 2000 Technische Universitaet Muenchen |
3 Copyright 2000 Technische Universitaet Muenchen |
4 *) |
4 *) |
5 |
5 |
6 section {* Monotonicity of eff and app *} |
6 section \<open>Monotonicity of eff and app\<close> |
7 |
7 |
8 theory EffectMono |
8 theory EffectMono |
9 imports Effect |
9 imports Effect |
10 begin |
10 begin |
11 |
11 |