src/HOL/Code_Evaluation.thy
changeset 42557 ae0deb39a254
parent 40884 3113fd4810bd
child 42979 5b9e16259341
equal deleted inserted replaced
42556:f65e5f0341b8 42557:ae0deb39a254