Re: [isabelle-dev] NEWS: 'consider' command and "cases" method

2015-09-23 Thread Manuel Eberl
Ah, interesting. Thanks! On 23/09/15 08:47, Andreas Lochbihler wrote: > Dear Manuel, > > consider supports the same syntax as obtains, i.e., you can use "where" > as in > > consider "x = ∞" | "x = -∞" | y where "x = ereal y" > > Andreas > > On 23/09/15 08:41, Manuel Eberl wrote: >> Is there

Re: [isabelle-dev] NEWS: 'consider' command and "cases" method

2015-09-23 Thread Andreas Lochbihler
Dear Manuel, consider supports the same syntax as obtains, i.e., you can use "where" as in consider "x = ∞" | "x = -∞" | y where "x = ereal y" Andreas On 23/09/15 08:41, Manuel Eberl wrote: Is there a way to use ‘consider’ with fixed variables? E.g. if I have a rule like ereal_cases: