changeset 34007 | aea892559fc5 |
parent 33988 | 901001414358 |
child 34065 | 6f8f9835e219 |
--- a/src/HOL/Predicate.thy Sat Dec 05 10:18:23 2009 +0100 +++ b/src/HOL/Predicate.thy Sat Dec 05 20:02:21 2009 +0100 @@ -726,7 +726,7 @@ proof (cases "f ()") case Empty thus ?thesis - unfolding Seq_def by (simp add: sup_commute [of "\<bottom>"] sup_bot) + unfolding Seq_def by (simp add: sup_commute [of "\<bottom>"]) next case Insert thus ?thesis