src/HOL/IMP/Examples.thy
changeset 23842 9d87177f1f89
parent 18372 2bffdf62fe7f
child 27362 a6dc1769fdda