src/HOL/Predicate.thy

--- a/src/HOL/Predicate.thy	Wed Sep 23 16:20:12 2009 +0200
+++ b/src/HOL/Predicate.thy	Wed Sep 23 16:20:12 2009 +0200
@@ -797,6 +797,10 @@
    (auto simp add: Seq_def the_only_singleton is_empty_def
       null_is_empty singleton_bot singleton_single singleton_sup Let_def)
 
+lemma meta_fun_cong:
+"f == g ==> f x == g x"
+by simp
+
 ML {*
 signature PREDICATE =
 sig