src/HOL/List.thy
changeset 8703 816d8f6513be
parent 8490 6e0f23304061
child 8873 ab920d8112b4
     1.1 --- a/src/HOL/List.thy	Thu Apr 13 15:01:45 2000 +0200
     1.2 +++ b/src/HOL/List.thy	Thu Apr 13 15:01:50 2000 +0200
     1.3 @@ -176,7 +176,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 (split op#) (split op#) `` (r ** lexn r n)) Int
     1.8 +"lexn r (Suc n) = (prod_fun (split op#) (split op#) `` (r <*lex*> lexn r n)) Int
     1.9                    {(xs,ys). length xs = Suc n & length ys = Suc n}"
    1.10  
    1.11  constdefs
    1.12 @@ -184,7 +184,7 @@
    1.13  "lex r == UN n. lexn r n"
    1.14  
    1.15   lexico :: "('a * 'a)set => ('a list * 'a list)set"
    1.16 -"lexico r == inv_image (less_than ** lex r) (%xs. (length xs, xs))"
    1.17 +"lexico r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
    1.18  
    1.19  end
    1.20