src/HOL/IMP/Examples.thy
changeset 27163 587ad1fba128
parent 18372 2bffdf62fe7f
child 27362 a6dc1769fdda