changeset 70749 | 5d06b7bb9d22 |
parent 66453 | cc19f7ca2ed6 |
child 73526 | a3cc9fa1295d |
--- a/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy Mon Sep 23 17:15:44 2019 +0200 +++ b/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy Tue Sep 24 12:56:10 2019 +0100 @@ -198,7 +198,7 @@ apply (rule ccontr) apply auto apply (drule injf_max_order_preserving2) - apply (metis linorder_antisym_conv3 order_less_le) + apply (metis antisym_conv3 order_less_le) done lemma infinite_set_has_order_preserving_inj: