changeset 10731 | f44ab3108202 |
parent 10433 | 6c5659d461dd |
child 11006 | e85c0e2f33d6 |
--- a/src/HOL/HOL_lemmas.ML Fri Dec 22 18:25:00 2000 +0100 +++ b/src/HOL/HOL_lemmas.ML Sat Dec 23 22:49:39 2000 +0100 @@ -472,7 +472,7 @@ (** Standard abbreviations **) -(* combination of (spec RS spec RS ...(j times) ... spec RS mp *) +(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *) local fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t | wrong_prem (Bound _) = true