src/HOL/Library/While_Combinator.thy
changeset 53425 f5b1f555b73b
parent 53381 355a4cac5440
child 54047 83fb090dae9e
equal deleted inserted replaced
53414:dd64696d267a 53425:f5b1f555b73b