# HG changeset patch # User nipkow # Date 1101921110 -3600 # Node ID 0de05d10406003f1601648368c04080ec8de6b95 # Parent 9234f5765d9c9b943cec476392c8404e3993ef22 Removed postfix >= because of new >= sugar diff -r 9234f5765d9c -r 0de05d104060 src/HOL/Library/List_Prefix.thy --- a/src/HOL/Library/List_Prefix.thy Wed Dec 01 18:11:13 2004 +0100 +++ b/src/HOL/Library/List_Prefix.thy Wed Dec 01 18:11:50 2004 +0100 @@ -215,7 +215,7 @@ subsection {* Postfix order on lists *} - +(* constdefs postfix :: "'a list => 'a list => bool" ("(_/ >= _)" [51, 50] 50) "xs >= ys == \zs. xs = zs @ ys" @@ -258,5 +258,5 @@ apply (rule_tac x = "rev zs" in exI) apply (rule rev_is_rev_conv [THEN iffD1], simp) done - +*) end