src/HOL/ex/Interpretation_with_Defs.thy
changeset 47133 89b13238d7f2
parent 46950 d0181abdbdac
child 48644 70a5d78e8326