src/HOL/Library/List_Prefix.thy
changeset 12338 de0f4a63baa5
parent 11987 bf31b35949ce
child 14300 bf8b8c9425c3
     1.1 --- a/src/HOL/Library/List_Prefix.thy	Sat Dec 01 18:51:46 2001 +0100
     1.2 +++ b/src/HOL/Library/List_Prefix.thy	Sat Dec 01 18:52:32 2001 +0100
     1.3 @@ -13,13 +13,13 @@
     1.4  
     1.5  subsection {* Prefix order on lists *}
     1.6  
     1.7 -instance list :: ("term") ord ..
     1.8 +instance list :: (type) ord ..
     1.9  
    1.10  defs (overloaded)
    1.11    prefix_def: "xs \<le> ys == \<exists>zs. ys = xs @ zs"
    1.12    strict_prefix_def: "xs < ys == xs \<le> ys \<and> xs \<noteq> (ys::'a list)"
    1.13  
    1.14 -instance list :: ("term") order
    1.15 +instance list :: (type) order
    1.16    by intro_classes (auto simp add: prefix_def strict_prefix_def)
    1.17  
    1.18  lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys"