named the primrec clauses of upt
authorpaulson
Fri, 26 May 2000 18:04:17 +0200
changeset 8983 15bd7d568fb2
parent 8982 4cb682fc083d
child 8984 b71c460c6f97
named the primrec clauses of upt
src/HOL/List.thy
--- 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)"