src/HOL/Extraction.thy
changeset 20984 d09f388fa9db
parent 20941 beedcae49096
child 22281 23e0fde84cb7
equal deleted inserted replaced
20983:d4500b9b220e 20984:d09f388fa9db