| changeset 20807 | bd3b60f9a343 |
| parent 19769 | c40ce2de2020 |
| child 21404 | eb85850d3eb7 |
--- a/src/HOL/Library/While_Combinator.thy Sun Oct 01 12:07:57 2006 +0200 +++ b/src/HOL/Library/While_Combinator.thy Sun Oct 01 18:29:23 2006 +0200 @@ -37,7 +37,7 @@ definition while :: "('a => bool) => ('a => 'a) => 'a => 'a" - "while b c s == while_aux (b, c, s)" + "while b c s = while_aux (b, c, s)" lemma while_aux_unfold: "while_aux (b, c, s) =