Re: [isabelle] Isabelle2015-RC2 available for testing



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.