src/HOL/List.thy
changeset 10832 e33b47e4246d
parent 9355 1b2cd40579c6
child 12114 a8e860c86252
     1.1 --- a/src/HOL/List.thy	Tue Jan 09 15:18:07 2001 +0100
     1.2 +++ b/src/HOL/List.thy	Tue Jan 09 15:22:13 2001 +0100
     1.3 @@ -177,7 +177,7 @@
     1.4   lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
     1.5  primrec
     1.6  "lexn r 0       = {}"
     1.7 -"lexn r (Suc n) = (prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) `` (r <*lex*> lexn r n)) Int
     1.8 +"lexn r (Suc n) = (prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) ` (r <*lex*> lexn r n)) Int
     1.9                    {(xs,ys). length xs = Suc n & length ys = Suc n}"
    1.10  
    1.11  constdefs