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.
> On 1 May 2015, at 15:32, C. Diekmann <diekmann at in.tum.de> wrote:
> I guess there are some superfluous lemmas in 2015-RC2 in Main:
> theory Scratch
> imports Main
> 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and