| changeset 35083 | 3246e66b0874 |
| parent 35050 | 9f841f20dca6 |
| child 36349 | 39be26d1bc28 |
--- a/src/HOL/NSA/StarDef.thy Wed Feb 10 08:49:25 2010 +0100 +++ b/src/HOL/NSA/StarDef.thy Wed Feb 10 08:49:26 2010 +0100 @@ -893,6 +893,7 @@ apply (intro_classes) apply (transfer, erule left_inverse) apply (transfer, erule right_inverse) +apply (transfer, fact divide_inverse) done instance star :: (field) field