src/HOL/Library/While_Combinator.thy
changeset 17201 3bdf1dfcdee4
parent 15197 19e735596e51
child 18372 2bffdf62fe7f
equal deleted inserted replaced
17200:3a4d03d1a31b 17201:3bdf1dfcdee4