# HG changeset patch
# User oheimb
# Date 905352194 -7200
# Node ID 45bd13b15d803eaadf312ae9e72d36088b05b81b
# Parent  f099dffd0f189e2a71de230adb51eae0378f74fe
added Id_apply

diff -r f099dffd0f18 -r 45bd13b15d80 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Wed Sep 09 16:42:45 1998 +0200
+++ b/src/HOL/Fun.ML	Wed Sep 09 16:43:14 1998 +0200
@@ -31,6 +31,12 @@
 qed "bchoice";
 
 
+section "Id";
+
+qed_goalw "Id_apply" thy [Id_def] "Id x = x" (K [rtac refl 1]);
+Addsimps [Id_apply];
+
+
 section "o";
 
 qed_goalw "o_apply" thy [o_def] "(f o g) x = f (g x)"