author | wenzelm |
Tue, 18 Jul 2000 14:52:30 +0200 | |
changeset 9382 | 7cea1cb9703e |
parent 9381 | a0491eed2270 |
child 9383 | c21fa1c48de0 |
--- 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"