diff -r aecf1ddf3541 -r c27f04bb2262 thys3/Blexer2.thy