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)