| changeset 972 | e61b058d58d2 |
| parent 965 | 24eef3860714 |
| child 1152 | b6e1e74695f6 |
--- a/src/HOL/Arith.ML Thu Mar 23 15:39:13 1995 +0100 +++ b/src/HOL/Arith.ML Fri Mar 24 12:30:35 1995 +0100 @@ -175,7 +175,7 @@ val wf_less_trans = wf_pred_nat RS wf_trancl RSN (2, def_wfrec RS trans); -goalw Nat.thy [less_def] "<m,n> : pred_nat^+ = (m<n)"; +goalw Nat.thy [less_def] "(m,n) : pred_nat^+ = (m<n)"; by (rtac refl 1); qed "less_eq";