src/HOL/Lex/Chopper.thy
changeset 7333 6cb15c6f1d9f
parent 2609 4370e5f0fa3f
child 10338 291ce4c4b50e
equal deleted inserted replaced
7332:60534b9018ae 7333:6cb15c6f1d9f