changeset 9382 | 7cea1cb9703e |
parent 6824 | 8f7bfd81a4c6 |
child 12338 | de0f4a63baa5 |
--- a/src/HOL/UNITY/GenPrefix.thy Tue Jul 18 13:16:48 2000 +0200 +++ b/src/HOL/UNITY/GenPrefix.thy Tue Jul 18 14:52:30 2000 +0200 @@ -27,7 +27,7 @@ append "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)" -arities list :: (term)ord +instance list :: (term)ord defs prefix_def "xs <= zs == (xs,zs) : genPrefix Id"