src/HOL/Library/While_Combinator.thy
changeset 45628 f21eb7073895
parent 41764 5268aef2fe83
child 45834 9c232d370244
equal deleted inserted replaced
45627:a0336f8b6558 45628:f21eb7073895