# HG changeset patch
# User oheimb
# Date 902933365 -7200
# Node ID 3d1368a3a2a275c460d23bcbd247ee8d5bbb9f35
# Parent  513925de8962c4cb7cdabea95b1cae068514302a
added theorems Id_o, o_Id
corrected name of theorem: fund_upd_other -> fun_upd_other

diff -r 513925de8962 -r 3d1368a3a2a2 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Wed Aug 12 16:23:25 1998 +0200
+++ b/src/HOL/Fun.ML	Wed Aug 12 16:49:25 1998 +0200
@@ -7,17 +7,6 @@
 *)
 
 
-qed_goalw "o_apply" thy [o_def] "(f o g) x = f (g x)"
- (K [rtac refl 1]);
-Addsimps [o_apply];
-
-qed_goalw "o_assoc" thy [o_def] "f o (g o h) = f o g o h"
-  (K [rtac ext 1, rtac refl 1]);
-
-Goalw [o_def] "(f o g)``r = f``(g``r)";
-by (Blast_tac 1);
-qed "image_compose";
-
 Goal "(f = g) = (!x. f(x)=g(x))";
 by (rtac iffI 1);
 by (Asm_simp_tac 1);
@@ -42,6 +31,30 @@
 qed "bchoice";
 
 
+section "o";
+
+qed_goalw "o_apply" thy [o_def] "(f o g) x = f (g x)"
+ (K [rtac refl 1]);
+Addsimps [o_apply];
+
+qed_goalw "o_assoc" thy [o_def] "f o (g o h) = f o g o h"
+  (K [rtac ext 1, rtac refl 1]);
+
+qed_goalw "Id_o" thy [Id_def] "Id o g = g"
+ (K [rtac ext 1, Simp_tac 1]);
+Addsimps [Id_o];
+
+qed_goalw "o_Id" thy [Id_def] "f o Id = f"
+ (K [rtac ext 1, Simp_tac 1]);
+Addsimps [o_Id];
+
+Goalw [o_def] "(f o g)``r = f``(g``r)";
+by (Blast_tac 1);
+qed "image_compose";
+
+
+section "inj";
+
 (*** inj(f): f is a one-to-one function ***)
 
 val prems = goalw thy [inj_def]
@@ -195,7 +208,7 @@
 
 qed_goal "fun_upd_same" thy "(f(x:=y)) x = y" 
 	(K [Simp_tac 1]);
-qed_goal "fund_upd_other" thy "!!X. z~=x ==> (f(x:=y)) z = f z"
+qed_goal "fun_upd_other" thy "!!X. z~=x ==> (f(x:=y)) z = f z"
 	(K [Asm_simp_tac 1]);
 (*Addsimps [fun_upd_same, fun_upd_other];*)