changeset 11655 | 923e4d0d36d5 |
parent 11454 | 7514e5e21cb8 |
child 13297 | e4ae0732e2be |
--- a/src/HOL/NatArith.thy Wed Oct 03 20:54:05 2001 +0200 +++ b/src/HOL/NatArith.thy Wed Oct 03 20:54:16 2001 +0200 @@ -9,8 +9,8 @@ setup arith_setup -lemma pred_nat_trancl_eq_le: "(m, n) : pred_nat^* = (m <= n)" -apply (simp add: less_eq reflcl_trancl [THEN sym] +lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m <= n)" +apply (simp add: less_eq reflcl_trancl [symmetric] del: reflcl_trancl) by arith