src/HOL/ex/Interpretation_with_Defs.thy
changeset 44457 d366fa5551ef
parent 41582 c34415351b6d
child 46950 d0181abdbdac