On Wed, 2 Oct 2013, Alexander Krauss wrote:
Nevertheless, it is also a bit irritating that there seems to be no
proper way of adding support for wildcards to fun_cases (and
inductive_cases). This should be addressed at some point, but for now we
are fine.
There is no fundamental problem to s
On 09/30/2013 02:41 PM, Makarius wrote:
On Mon, 30 Sep 2013, Manuel Eberl wrote:
On 30/09/13 11:49, Makarius wrote:
On Mon, 23 Sep 2013, Manuel Eberl wrote:
I sent my changes to Alexander Krauss last Wednesday so that he can
review them.
We are now getting very close to the fork-point for
On Mon, 30 Sep 2013, Manuel Eberl wrote:
On 30/09/13 11:49, Makarius wrote:
On Mon, 23 Sep 2013, Manuel Eberl wrote:
I sent my changes to Alexander Krauss last Wednesday so that he can
review them.
We are now getting very close to the fork-point for the release. So
can you just post the ch
On 30/09/13 11:49, Makarius wrote:
> On Mon, 23 Sep 2013, Manuel Eberl wrote:
>
>> I sent my changes to Alexander Krauss last Wednesday so that he can
>> review them.
>
> We are now getting very close to the fork-point for the release. So
> can you just post the changeset here, or send it to me pr
On Mon, 23 Sep 2013, Manuel Eberl wrote:
I sent my changes to Alexander Krauss last Wednesday so that he can
review them.
We are now getting very close to the fork-point for the release. So can
you just post the changeset here, or send it to me privately?
Makarius
Hallo,
I just remembered that I wanted to tell you that I have done what you
asked and set everything up in exactly the same way that inductive_cases
does it. I sent my changes to Alexander Krauss last Wednesday so that he
can review them.
Cheers,
Manuel
On 09/17/2013 06:19 PM, Makarius wrote:
>
On Tue, 17 Sep 2013, Manuel Eberl wrote:
With the documentation on Isabelle/ML being so sparse, one is, as a
beginner, all but forced to experiment with snippets of code from other
parts of Isabelle until stuff works, and that's what I did.
The documentation is both too much and too little.
On 17/09/13 00:13, Makarius wrote:
> When you have an Isar command, its main functionality needs to be
> available directly in ML as well. That is an automatism, without
> thinking. For the opposite you would have to provide a proof over
> future uses of your tool.
>
> There is a certain standard
On Tue, 17 Sep 2013, Manuel Eberl wrote:
The main thing still missing in Isabelle/5ccee1cb245a is a regular ML
interface Fun_Cases.fun_cases.
What do you mean by that? There exists an ML function
Fun_Cases.mk_fun_cases : Proof.context -> term -> thm -- is that not an
ML interface to the Fun_Cas
Hallo,
> The main thing still missing in Isabelle/5ccee1cb245a is a regular ML
> interface Fun_Cases.fun_cases.
What do you mean by that? There exists an ML function
Fun_Cases.mk_fun_cases : Proof.context -> term -> thm -- is that not an
ML interface to the Fun_Cases tool? Or do you also want a fun
On Fri, 13 Sep 2013, Alexander Krauss wrote:
This refers to Isabelle f557a4645f61:
* New command "fun_cases" derives ad-hoc elimination rules for
function equations as simplified instances of f.elims, analogous to
inductive_cases. See HOL/ex/Fundefs.thy for some examples.
Thanks. I see that
This refers to Isabelle f557a4645f61:
* Function package: For mutually recursive functions f and g, separate
cases rules f.cases and g.cases are generated instead of unusable
f_g.cases which exposed internal sum types. Potential INCOMPATIBILITY,
in the case that the unusable rule was used neverth
12 matches
Mail list logo
