Re: [isabelle-dev] Interpretation [was HOL/ex/Set_Algebras]

2012-04-19 Thread Clemens Ballarin
Hi Florian, I understood that much. What I was hoping for was an answer on a more technical level. The definition + interpretation pattern seem a useful thing to have. But it sounds like, if you change the main interpretation command like this, you will break it for intended use cases

Re: [isabelle-dev] Interpretation [was HOL/ex/Set_Algebras]

2012-04-19 Thread Makarius
On Thu, 19 Apr 2012, Clemens Ballarin wrote: Maybe what you want is an alternative command to 'interpretation'. Creating definitions from definition to me is not interpreting something in some other context by means of existing entities, but creating a new instance of something. The