src/HOL/IMP/Examples.thy
changeset 20700 7e3450c10c2d
parent 18372 2bffdf62fe7f
child 27362 a6dc1769fdda