| changeset 12338 | de0f4a63baa5 |
| parent 9382 | 7cea1cb9703e |
--- a/src/HOL/UNITY/GenPrefix.thy Sat Dec 01 18:51:46 2001 +0100 +++ b/src/HOL/UNITY/GenPrefix.thy Sat Dec 01 18:52:32 2001 +0100 @@ -27,7 +27,7 @@ append "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)" -instance list :: (term)ord +instance list :: (type)ord defs prefix_def "xs <= zs == (xs,zs) : genPrefix Id"