src/HOL/Library/MLString.thy
2006-08-30 haftmann 2006-08-30 code refinements
2006-08-21 haftmann 2006-08-21 added some codegen examples/applications