src/HOL/Library/While_Combinator.thy
changeset 37460 910b2422571d
parent 30738 0842e906300c
child 37757 dc78d2d9e90a
equal deleted inserted replaced
37459:7a3610dca96b 37460:910b2422571d