src/HOL/List.thy
changeset 9336 9ae89b9ce206
parent 8983 15bd7d568fb2
child 9341 40bab6613000
     1.1 --- a/src/HOL/List.thy	Fri Jul 14 14:46:35 2000 +0200
     1.2 +++ b/src/HOL/List.thy	Fri Jul 14 14:47:15 2000 +0200
     1.3 @@ -181,11 +181,14 @@
     1.4                    {(xs,ys). length xs = Suc n & length ys = Suc n}"
     1.5  
     1.6  constdefs
     1.7 - lex :: "('a * 'a)set => ('a list * 'a list)set"
     1.8 -"lex r == UN n. lexn r n"
     1.9 +  lex :: "('a * 'a)set => ('a list * 'a list)set"
    1.10 +    "lex r == UN n. lexn r n"
    1.11  
    1.12 - lexico :: "('a * 'a)set => ('a list * 'a list)set"
    1.13 -"lexico r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
    1.14 +  lexico :: "('a * 'a)set => ('a list * 'a list)set"
    1.15 +    "lexico r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
    1.16 +
    1.17 +  sublist :: "['a list, nat set] => 'a list"
    1.18 +    "sublist xs A == map fst (filter (%p. snd p : A) (zip xs [0..size xs(]))"
    1.19  
    1.20  end
    1.21