src/HOL/Library/While_Combinator.thy
changeset 49088 5cd8b4426a57
parent 46365 547d1a1dcaf6
child 50008 eb7f574d0303
equal deleted inserted replaced
49087:7a17ba4bc997 49088:5cd8b4426a57