| changeset 27682 | 25aceefd4786 |
| parent 27651 | 16a26996c30e |
| child 28059 | 295a8fc92684 |
--- a/src/HOL/NSA/StarDef.thy Fri Jul 25 12:03:32 2008 +0200 +++ b/src/HOL/NSA/StarDef.thy Fri Jul 25 12:03:34 2008 +0200 @@ -732,7 +732,7 @@ instance star :: (order) order apply (intro_classes) -apply (transfer, rule order_less_le) +apply (transfer, rule less_le_not_le) apply (transfer, rule order_refl) apply (transfer, erule (1) order_trans) apply (transfer, erule (1) order_antisym)