src/HOL/Isar_examples/W_correct.thy
changeset 9450 c97dba47e504
parent 8491 82826ed95d4b
child 9475 b24516d96847