src/HOL/Extraction.thy
changeset 44408 30ea62ab4f16
parent 37233 b78f31ca4675
child 48891 c0eafbd55de3
equal deleted inserted replaced
44407:7b6629037127 44408:30ea62ab4f16