src/HOL/Library/While_Combinator.thy
changeset 55013 869f50dfdad2
parent 54196 0c188a3c671a
child 55466 786edc984c98
equal deleted inserted replaced
55011:e2042c4ae1b7 55013:869f50dfdad2