named the primrec clauses of upt
authorpaulson
Fri May 26 18:04:17 2000 +0200 (2000-05-26)
changeset 898315bd7d568fb2
parent 8982 4cb682fc083d
child 8984 b71c460c6f97
named the primrec clauses of upt
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Fri May 26 18:03:54 2000 +0200
     1.2 +++ b/src/HOL/List.thy	Fri May 26 18:04:17 2000 +0200
     1.3 @@ -155,8 +155,8 @@
     1.4    (* Warning: simpset does not contain this definition but separate theorems 
     1.5       for xs=[] / xs=z#zs *)
     1.6  primrec
     1.7 -  "[i..0(] = []"
     1.8 -  "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"
     1.9 +  upt_0   "[i..0(] = []"
    1.10 +  upt_Suc "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"
    1.11  primrec
    1.12    "nodups []     = True"
    1.13    "nodups (x#xs) = (x ~: set xs & nodups xs)"