src/HOL/ex/Codegenerator.thy
changeset 26161 34cb0b457dcc
parent 24810 862b71696efe
child 28335 25326092cf9a
equal deleted inserted replaced
26160:ff5bb2b532b3 26161:34cb0b457dcc