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
Net.unify_term.

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


	Makarius





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