author | nipkow |
Wed, 01 Dec 2004 18:11:50 +0100 | |
changeset 15355 | 0de05d104060 |
parent 15354 | 9234f5765d9c |
child 15356 | cfd08f5e0bdd |
--- 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