src/HOL/Library/While_Combinator.thy
changeset 19903 158ea5884966
parent 19769 c40ce2de2020
child 20807 bd3b60f9a343
equal deleted inserted replaced
19902:9e5d0df75c98 19903:158ea5884966