author | wenzelm |
Sat, 23 Dec 2000 22:49:39 +0100 | |
changeset 10731 | f44ab3108202 |
parent 10730 | bbaa0c6ef59f |
child 10732 | d4fda7d05ce5 |
--- 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