src/HOL/ex/PER.thy
changeset 69565 1daf07b65385
parent 61933 cf58b5b794b2
child 69597 ff784d5a5bfb
equal deleted inserted replaced
69564:a59f7d07bf17 69565:1daf07b65385