# HG changeset patch
# User paulson
# Date 950177322 -3600
# Node ID 07284f7ad26211d419c16d636c6f61eac3d91491
# Parent  fc5db20d7f6f235da31babc46b83f30358d07ab5
new thm and simprule inv_id

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";