Re: [isabelle] Isabelle2015-RC2 available for testing

This is more an indication of the flexibility of Isabelleâs inference mechanisms that you can solve the goal

	x = x

in one single step by applying the rule

	?f (Basic_BNF_LFPs.xtor ?x) = ?f ?x


 	?R (Basic_BNF_LFPs.xtor ?x) (Basic_BNF_LFPs.xtor ?y) = ?R ?x ?y .

Iâm sure that these theorems, in the form given, serve some useful purpose.

Larry Paulson

> On 1 May 2015, at 15:32, C. Diekmann <diekmann at> wrote:
> Hi,
> I guess there are some superfluous lemmas in 2015-RC2 in Main:
> theory Scratch
> imports Main
> begin
> lemma "x = x"
> Auto solve_direct: The current goal can be solved directly with
>  BNF_Composition.DEADID.map_ident: ?t = ?t
>  BNF_Composition.DEADID.rel_refl: ?x = ?x
>  Basic_BNF_LFPs.xtor_rel: ?R (Basic_BNF_LFPs.xtor ?x)
> (Basic_BNF_LFPs.xtor ?y) = ?R ?x ?y
>  Basic_BNF_LFPs.xtor_set: ?f (Basic_BNF_LFPs.xtor ?x) = ?f ?x
>  HOL.refl: ?t = ?t
> Cheers,
>  Cornelius

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.