# HG changeset patch
# User paulson
# Date 959357057 -7200
# Node ID 15bd7d568fb21054649ce397efe77050321d3c0e
# Parent  4cb682fc083d6eb907c54c2625a344d41cc9d0cb
named the primrec clauses of upt

diff -r 4cb682fc083d -r 15bd7d568fb2 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)"