Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/List_Prefix.thy
changeset 12338 de0f4a63baa5
parent 11987 bf31b35949ce
child 14300 bf8b8c9425c3 
--- a/src/HOL/Library/List_Prefix.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Library/List_Prefix.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -13,13 +13,13 @@
 
 subsection {* Prefix order on lists *}
 
-instance list :: ("term") ord ..
+instance list :: (type) ord ..
 
 defs (overloaded)
   prefix_def: "xs \<le> ys == \<exists>zs. ys = xs @ zs"
   strict_prefix_def: "xs < ys == xs \<le> ys \<and> xs \<noteq> (ys::'a list)"
 
-instance list :: ("term") order
+instance list :: (type) order
   by intro_classes (auto simp add: prefix_def strict_prefix_def)
 
 lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys"
isabelle