# HG changeset patch
# User haftmann
# Date 1163428984 -3600
# Node ID 2b3c41d02e87925dca812c82117fb3648d815be0
# Parent  c33cdc5a6c7c897278a181c5a65caa4cc98a6687
dropped Typedef dependency

diff -r c33cdc5a6c7c -r 2b3c41d02e87 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Mon Nov 13 15:43:03 2006 +0100
+++ b/src/HOL/Fun.thy	Mon Nov 13 15:43:04 2006 +0100
@@ -7,13 +7,9 @@
 header {* Notions about functions *}
 
 theory Fun
-imports Typedef
+imports Set
 begin
 
-instance set :: (type) order
-  by (intro_classes,
-      (assumption | rule subset_refl subset_trans subset_antisym psubset_eq)+)
-
 constdefs
   fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)"
    "fun_upd f a b == % x. if x=a then b else f x"
@@ -77,10 +73,11 @@
 
 text{*As a simplification rule, it replaces all function equalities by
   first-order equalities.*}
-lemma expand_fun_eq: "(f = g) = (! x. f(x)=g(x))"
+lemma expand_fun_eq: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
 apply (rule iffI)
 apply (simp (no_asm_simp))
-apply (rule ext, simp (no_asm_simp))
+apply (rule ext)
+apply (simp (no_asm_simp))
 done
 
 lemma apply_inverse: