| changeset 30198 | 922f944f03b2 |
| parent 30082 | 43c5b7bfc791 |
| child 30242 | aea5d7fa7ef5 |
--- a/src/HOL/RealDef.thy Mon Mar 02 08:26:03 2009 +0100 +++ b/src/HOL/RealDef.thy Mon Mar 02 16:53:55 2009 +0100 @@ -94,7 +94,7 @@ by (simp add: realrel_def) lemma equiv_realrel: "equiv UNIV realrel" -apply (auto simp add: equiv_def refl_def sym_def trans_def realrel_def) +apply (auto simp add: equiv_def refl_on_def sym_def trans_def realrel_def) apply (blast dest: preal_trans_lemma) done