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