src/HOL/Induct/Term.ML
changeset 5707 b0e631634b5a
parent 5278 a903b66822e2
child 5738 0d8698c15439
equal deleted inserted replaced
5706:21706a735c8d 5707:b0e631634b5a