Re: [isabelle] qed and done take long for large goal states
- To: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>
- Subject: Re: [isabelle] qed and done take long for large goal states
- From: Makarius <makarius at sketis.net>
- Date: Tue, 9 Aug 2016 23:40:25 +0200
- In-reply-to: <email@example.com>
- References: <577E0CB2.firstname.lastname@example.org> <email@example.com> <firstname.lastname@example.org> <email@example.com> <firstname.lastname@example.org>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.2.0
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