src/HOL/IMPP/Com.thy
changeset 13240 bb5f4faea1f3
parent 12338 de0f4a63baa5
child 17477 ceb42ea2f223