# 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 == \<exists>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