src/HOL/Library/While_Combinator.thy
changeset 60806 622d45ca75ee
parent 60580 7e741e22d7fc
child 61115 3a4400985780
equal deleted inserted replaced
60804:080a979a985b 60806:622d45ca75ee