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"
```