equal
deleted
inserted
replaced
730 |
730 |
731 subsection {* Ordering and lattice classes *} |
731 subsection {* Ordering and lattice classes *} |
732 |
732 |
733 instance star :: (order) order |
733 instance star :: (order) order |
734 apply (intro_classes) |
734 apply (intro_classes) |
735 apply (transfer, rule order_less_le) |
735 apply (transfer, rule less_le_not_le) |
736 apply (transfer, rule order_refl) |
736 apply (transfer, rule order_refl) |
737 apply (transfer, erule (1) order_trans) |
737 apply (transfer, erule (1) order_trans) |
738 apply (transfer, erule (1) order_antisym) |
738 apply (transfer, erule (1) order_antisym) |
739 done |
739 done |
740 |
740 |