--- a/src/HOL/UNITY/Follows.thy Mon Sep 21 12:24:21 2009 +0200
+++ b/src/HOL/UNITY/Follows.thy Mon Sep 21 14:23:04 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/UNITY/Follows
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
*)
@@ -160,7 +159,7 @@
lemma Follows_Un:
"[| F \<in> f' Fols f; F \<in> g' Fols g |]
==> F \<in> (%s. (f' s) \<union> (g' s)) Fols (%s. (f s) \<union> (g s))"
-apply (simp add: Follows_def Increasing_Un Always_Un del: Un_subset_iff, auto)
+apply (simp add: Follows_def Increasing_Un Always_Un del: Un_subset_iff le_sup_iff, auto)
apply (rule LeadsTo_Trans)
apply (blast intro: Follows_Un_lemma)
(*Weakening is used to exchange Un's arguments*)