src/HOL/Library/While_Combinator.thy
changeset 53730 f2f6874893df
parent 53381 355a4cac5440
child 54047 83fb090dae9e
equal deleted inserted replaced
53729:b9d727a767ea 53730:f2f6874893df