# HG changeset patch
# User huffman
# Date 1126052004 -7200
# Node ID 6c82a5c1007605a543a257b1412a9e5c965fc8bd
# Parent  5798fbf42a6ac9bf4ea59c674ece6e87ad1c1eb3
added theorem hypreal_inverse2

diff -r 5798fbf42a6a -r 6c82a5c10076 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Wed Sep 07 01:49:49 2005 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Wed Sep 07 02:13:24 2005 +0200
@@ -382,6 +382,10 @@
 apply simp
 done
 
+lemma hypreal_inverse2 [unfolded star_n_def]: 
+      "inverse (star_n X) = star_n (%n. inverse(X n))"
+by (simp add: star_inverse_def Ifun_of_def star_of_def Ifun_star_n)
+
 lemma hypreal_mult_inverse: 
      "x \<noteq> 0 ==> x*inverse(x) = (1::hypreal)"
 by (rule right_inverse)