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