src/HOL/Lex/Chopper.thy
changeset 6980 bb526ba7ba5f
parent 2609 4370e5f0fa3f
child 10338 291ce4c4b50e
equal deleted inserted replaced
6979:4b9963810121 6980:bb526ba7ba5f