diff -r fc5db20d7f6f -r 07284f7ad262 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Thu Feb 10 11:03:54 2000 +0100
+++ b/src/HOL/Fun.ML	Thu Feb 10 11:08:42 2000 +0100
@@ -38,6 +38,11 @@
 qed "id_apply";
 Addsimps [id_apply];
 
+Goal "inv id = id";
+by (simp_tac (simpset() addsimps [inv_def,id_def]) 1);
+qed "inv_id";
+Addsimps [inv_id];
+
 
 section "o";