src/HOL/Extraction.thy
changeset 18508 c5861e128a95
parent 18456 8cc35e95450a
child 18511 beed2bc052a3