Removed postfix >= because of new >= sugar
authornipkow
Wed, 01 Dec 2004 18:11:50 +0100
changeset 15355 0de05d104060
parent 15354 9234f5765d9c
child 15356 cfd08f5e0bdd
Removed postfix >= because of new >= sugar
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