| changeset 42150 | b0c0638c4aad |
| parent 34915 | 7894c7dab132 |
| child 56073 | 29e308b56d23 |
--- a/src/HOL/MicroJava/BV/EffectMono.thy Tue Mar 29 14:27:44 2011 +0200 +++ b/src/HOL/MicroJava/BV/EffectMono.thy Tue Mar 29 17:30:26 2011 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/MicroJava/BV/EffMono.thy +(* Title: HOL/MicroJava/BV/EffectMono.thy Author: Gerwin Klein Copyright 2000 Technische Universitaet Muenchen *)