src/HOL/Library/While_Combinator.thy
changeset 28985 af325cd29b15
parent 27487 c8a6ce181805
child 30738 0842e906300c
equal deleted inserted replaced
28984:060832a1f087 28985:af325cd29b15