src/HOL/Library/List_Prefix.thy
 changeset 19086 1b3780be6cc2 parent 18730 843da46f89ac child 21305 d41eddfd2b66
```     1.1 --- a/src/HOL/Library/List_Prefix.thy	Thu Feb 16 21:11:58 2006 +0100
1.2 +++ b/src/HOL/Library/List_Prefix.thy	Thu Feb 16 21:12:00 2006 +0100
1.3 @@ -155,9 +155,9 @@
1.4
1.5  subsection {* Parallel lists *}
1.6
1.7 -constdefs
1.8 +definition
1.9    parallel :: "'a list => 'a list => bool"    (infixl "\<parallel>" 50)
1.10 -  "xs \<parallel> ys == \<not> xs \<le> ys \<and> \<not> ys \<le> xs"
1.11 +  "(xs \<parallel> ys) = (\<not> xs \<le> ys \<and> \<not> ys \<le> xs)"
1.12
1.13  lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys"
1.14    unfolding parallel_def by blast
1.15 @@ -215,9 +215,9 @@
1.16
1.17  subsection {* Postfix order on lists *}
1.18
1.19 -constdefs
1.20 +definition
1.21    postfix :: "'a list => 'a list => bool"  ("(_/ >>= _)" [51, 50] 50)
1.22 -  "xs >>= ys == \<exists>zs. xs = zs @ ys"
1.23 +  "(xs >>= ys) = (\<exists>zs. xs = zs @ ys)"
1.24
1.25  lemma postfix_refl [simp, intro!]: "xs >>= xs"
1.26    by (auto simp add: postfix_def)
```