src/HOL/HOLCF/IOA/NTP/Correctness.thy
changeset 58270 16648edf16e3
parent 51703 f2e92fc0c8aa
child 58880 0baae4311a9f
     1.1 --- a/src/HOL/HOLCF/IOA/NTP/Correctness.thy	Tue Sep 09 20:51:36 2014 +0200
     1.2 +++ b/src/HOL/HOLCF/IOA/NTP/Correctness.thy	Tue Sep 09 20:51:36 2014 +0200
     1.3 @@ -89,7 +89,7 @@
     1.4  apply (simp add: hom_ioas)
     1.5  apply (blast dest!: add_leD1 [THEN leD])
     1.6  
     1.7 -apply (case_tac "m = hd (sq (sen (s)))")
     1.8 +apply (rename_tac m, case_tac "m = hd (sq (sen (s)))")
     1.9  
    1.10  apply force
    1.11