src/HOL/Library/While_Combinator.thy
changeset 63414 beb987127d0f
parent 63040 eb4ddd18d635
child 63561 fba08009ff3e
equal deleted inserted replaced
63413:9fe2d9dc095e 63414:beb987127d0f