src/HOL/Library/Pattern_Aliases.thy
changeset 72278 199dc903131b
parent 69597 ff784d5a5bfb
child 74383 107941e8fa01
equal deleted inserted replaced
72277:48254fa33d88 72278:199dc903131b