Removed postfix >= because of new >= sugar
authornipkow
Wed Dec 01 18:11:50 2004 +0100 (2004-12-01)
changeset 153550de05d104060
parent 15354 9234f5765d9c
child 15356 cfd08f5e0bdd
Removed postfix >= because of new >= sugar
src/HOL/Library/List_Prefix.thy
     1.1 --- a/src/HOL/Library/List_Prefix.thy	Wed Dec 01 18:11:13 2004 +0100
     1.2 +++ b/src/HOL/Library/List_Prefix.thy	Wed Dec 01 18:11:50 2004 +0100
     1.3 @@ -215,7 +215,7 @@
     1.4  
     1.5  
     1.6  subsection {* Postfix order on lists *}
     1.7 -
     1.8 +(*
     1.9  constdefs
    1.10    postfix :: "'a list => 'a list => bool"  ("(_/ >= _)" [51, 50] 50)
    1.11    "xs >= ys == \<exists>zs. xs = zs @ ys"
    1.12 @@ -258,5 +258,5 @@
    1.13    apply (rule_tac x = "rev zs" in exI)
    1.14    apply (rule rev_is_rev_conv [THEN iffD1], simp)
    1.15    done
    1.16 -
    1.17 +*)
    1.18  end