Re: [isabelle] qed and done take long for large goal states

On 03/08/16 09:34, Andreas Lochbihler wrote:
> I manually changed the appropriate
> line for Isabelle2016 and processing got indeed a bit faster.
> Unfortunately, abbreviations are no longer contracted as they were if
> eta-expanded terms are involved. For example,
>   abbreviation "rel R â list_all2 (rel_option R)"
>   term "list_all2 (rel_option undefined)"
>   term "list_all2 (Îx. rel_option undefined x)"
> Before the change, both "term" command output "rel undefined". After the
> change, the second prints "list_all2 (rel_option undefined)".

This requires more rethinking of the approach.

Net.match_term explicitly says "MUST BE BETA-ETA NORMAL", in contrast to

I am unsure if the net operations can be refined to cope with non-normal


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