| changeset 40431 | 682d6c455670 |
| parent 40430 | 483a4876e428 |
| child 40771 | 1c6f7d4b110e |
--- a/src/HOLCF/FOCUS/Stream_adm.thy Wed Nov 03 15:31:24 2010 -0700 +++ b/src/HOLCF/FOCUS/Stream_adm.thy Wed Nov 03 15:47:46 2010 -0700 @@ -157,7 +157,7 @@ apply ( fast) apply (unfold linorder_not_less) apply (drule (1) mp) -apply (erule all_dupE, drule mp, rule refl_less) +apply (erule all_dupE, drule mp, rule below_refl) apply (erule ssubst) apply (erule allE, drule (1) mp) apply (drule_tac P="%x. x" in subst, assumption)