src/HOL/MicroJava/J/JTypeSafe.thy
changeset 58860 fee7cfa69c50
parent 58263 6c907aad90ba
child 58886 8a6cac7c7247
     1.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -357,7 +357,7 @@
     1.4  apply(unfold is_class_def)
     1.5  apply(clarsimp)
     1.6  
     1.7 -apply(rule Call_type_sound);
     1.8 +apply(rule Call_type_sound)
     1.9  prefer 11
    1.10  apply blast
    1.11  apply (simp (no_asm_simp))+