| changeset 18215 | a28879118978 |
| parent 17428 | 8a2de150b5f1 |
| child 18429 | 42ee9f24f63a |
--- a/src/HOL/Real/PReal.thy Mon Nov 21 10:44:14 2005 +0100 +++ b/src/HOL/Real/PReal.thy Mon Nov 21 11:14:11 2005 +0100 @@ -24,7 +24,7 @@ lemma interval_empty_iff: "({y::'a::ordered_field. x < y & y < z} = {}) = (~(x < z))" -by (blast dest: dense intro: order_less_trans) +by (auto dest: dense) constdefs