src/HOL/IMP/Examples.thy
changeset 21966 edab0ecfbd7c
parent 18372 2bffdf62fe7f
child 27362 a6dc1769fdda