src/HOL/Induct/ABexp.thy
changeset 29690 c81f8b2967e1
parent 16417 9bc16273c2d4
child 36862 952b2b102a0a
equal deleted inserted replaced
29689:dd086f26ee4f 29690:c81f8b2967e1