| changeset 21404 | eb85850d3eb7 |
| parent 20503 | 503ac4c5ef91 |
| child 22270 | 4ccb7e6be929 |
--- a/src/HOL/Lambda/ListOrder.thy Fri Nov 17 02:19:55 2006 +0100 +++ b/src/HOL/Lambda/ListOrder.thy Fri Nov 17 02:20:03 2006 +0100 @@ -14,7 +14,7 @@ *} definition - step1 :: "('a \<times> 'a) set => ('a list \<times> 'a list) set" + step1 :: "('a \<times> 'a) set => ('a list \<times> 'a list) set" where "step1 r = {(ys, xs). \<exists>us z z' vs. xs = us @ z # vs \<and> (z', z) \<in> r \<and> ys = us @ z' # vs}"