src/HOL/Library/List_Prefix.thy
changeset 21404 eb85850d3eb7
parent 21305 d41eddfd2b66
child 22178 29b95968272b
     1.1 --- a/src/HOL/Library/List_Prefix.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Library/List_Prefix.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -159,7 +159,7 @@
     1.4  subsection {* Parallel lists *}
     1.5  
     1.6  definition
     1.7 -  parallel :: "'a list => 'a list => bool"    (infixl "\<parallel>" 50)
     1.8 +  parallel :: "'a list => 'a list => bool"  (infixl "\<parallel>" 50) where
     1.9    "(xs \<parallel> ys) = (\<not> xs \<le> ys \<and> \<not> ys \<le> xs)"
    1.10  
    1.11  lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys"
    1.12 @@ -218,7 +218,7 @@
    1.13  subsection {* Postfix order on lists *}
    1.14  
    1.15  definition
    1.16 -  postfix :: "'a list => 'a list => bool"  ("(_/ >>= _)" [51, 50] 50)
    1.17 +  postfix :: "'a list => 'a list => bool"  ("(_/ >>= _)" [51, 50] 50) where
    1.18    "(xs >>= ys) = (\<exists>zs. xs = zs @ ys)"
    1.19  
    1.20  lemma postfixI [intro?]: "xs = zs @ ys ==> xs >>= ys"