author | paulson |
Fri, 26 May 2000 18:04:17 +0200 | |
changeset 8983 | 15bd7d568fb2 |
parent 8982 | 4cb682fc083d |
child 8984 | b71c460c6f97 |
src/HOL/List.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/List.thy Fri May 26 18:03:54 2000 +0200 +++ b/src/HOL/List.thy Fri May 26 18:04:17 2000 +0200 @@ -155,8 +155,8 @@ (* Warning: simpset does not contain this definition but separate theorems for xs=[] / xs=z#zs *) primrec - "[i..0(] = []" - "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])" + upt_0 "[i..0(] = []" + upt_Suc "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])" primrec "nodups [] = True" "nodups (x#xs) = (x ~: set xs & nodups xs)"