# HG changeset patch
# User nipkow
# Date 1283935555 -7200
# Node ID 297cd703f1f0738f63d3a06678f522d584d33675
# Parent  3989b2b44dbaf0e38cbee3a08d6e26d2936a6542
put expand_(fun/set)_eq back in as synonyms, for compatibility

diff -r 3989b2b44dba -r 297cd703f1f0 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue Sep 07 15:56:33 2010 -0700
+++ b/src/HOL/Fun.thy	Wed Sep 08 10:45:55 2010 +0200
@@ -18,6 +18,8 @@
 apply (simp (no_asm_simp))
 done
 
+lemmas expand_fun_eq = ext_iff
+
 lemma apply_inverse:
   "f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
   by auto
diff -r 3989b2b44dba -r 297cd703f1f0 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Sep 07 15:56:33 2010 -0700
+++ b/src/HOL/Set.thy	Wed Sep 08 10:45:55 2010 +0200
@@ -498,6 +498,8 @@
 lemma set_ext_iff [no_atp]: "(A = B) = (ALL x. (x:A) = (x:B))"
 by(auto intro:set_ext)
 
+lemmas expand_set_eq [no_atp] = set_ext_iff
+
 lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
   -- {* Anti-symmetry of the subset relation. *}
   by (iprover intro: set_ext subsetD)