src/HOL/ex/Interpretation_with_Defs.thy
2011-01-15 haftmann 2011-01-15 experimental variant of interpretation with simultaneous definitions, plus example