src/HOL/Library/Fun_Lexorder.thy
changeset 73125 70eabc309de9
parent 68312 e9b5f25f6712
equal deleted inserted replaced
73124:802647edfe7b 73125:70eabc309de9