equal
deleted
inserted
replaced
25 prepend "[| (xs,ys) : genPrefix(r); (x,y) : r |] ==> |
25 prepend "[| (xs,ys) : genPrefix(r); (x,y) : r |] ==> |
26 (x#xs, y#ys) : genPrefix(r)" |
26 (x#xs, y#ys) : genPrefix(r)" |
27 |
27 |
28 append "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)" |
28 append "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)" |
29 |
29 |
30 instance list :: (term)ord |
30 instance list :: (type)ord |
31 |
31 |
32 defs |
32 defs |
33 prefix_def "xs <= zs == (xs,zs) : genPrefix Id" |
33 prefix_def "xs <= zs == (xs,zs) : genPrefix Id" |
34 |
34 |
35 strict_prefix_def "xs < zs == xs <= zs & xs ~= (zs::'a list)" |
35 strict_prefix_def "xs < zs == xs <= zs & xs ~= (zs::'a list)" |