| changeset 40009 | f2c78550c0b7 |
| parent 39159 | 0dec18004e75 |
| child 40087 | 1b5f394866d9 |
--- a/src/HOLCF/FOCUS/Fstream.thy Tue Oct 12 09:08:27 2010 -0700 +++ b/src/HOLCF/FOCUS/Fstream.thy Tue Oct 12 09:32:21 2010 -0700 @@ -95,7 +95,7 @@ apply (safe) apply (erule_tac [!] contrapos_np) prefer 2 apply (fast elim: DefE) -apply (rule Lift_cases) +apply (rule lift.exhaust) apply (erule (1) notE) apply (safe) apply (drule Def_inject_less_eq [THEN iffD1])