src/HOL/List.thy
changeset 8115 c802042066e8
parent 8000 acafa0f15131
child 8490 6e0f23304061
     1.1 --- a/src/HOL/List.thy	Fri Jan 07 11:06:03 2000 +0100
     1.2 +++ b/src/HOL/List.thy	Mon Jan 10 16:06:43 2000 +0100
     1.3 @@ -19,6 +19,7 @@
     1.4    hd, last    :: 'a list => 'a
     1.5    set         :: 'a list => 'a set
     1.6    list_all    :: ('a => bool) => ('a list => bool)
     1.7 +  list_all2   :: ('a => 'b => bool) => 'a list => 'b list => bool
     1.8    map         :: ('a=>'b) => ('a list => 'b list)
     1.9    mem         :: ['a, 'a list] => bool                    (infixl 55)
    1.10    nth         :: ['a list, nat] => 'a			  (infixl "!" 100)
    1.11 @@ -164,6 +165,10 @@
    1.12  primrec
    1.13    replicate_0   "replicate  0      x = []"
    1.14    replicate_Suc "replicate (Suc n) x = x # replicate n x"
    1.15 +defs
    1.16 + list_all2_def
    1.17 + "list_all2 P xs ys == length xs = length ys & (!(x,y):set(zip xs ys). P x y)"
    1.18 +
    1.19  
    1.20  (** Lexicographic orderings on lists **)
    1.21