Re: [isabelle] Eisbach: fold and named_theorems
Indeed, "unfold relator_eq[symmetric]" works in the method definition, but "fold
relator_eq" does not. Weird. I always considered fold and unfold to be the same up to the
orientation of the equation.
On 11/08/16 09:03, Peter Gammie wrote:
Did you try âunfold relator_eq[symmetric]â? I donât know how fold is implemented, so it may actually do this under the covers.
On 11 Aug 2016, at 16:59, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote:
Dear Eisbach gurus,
I'd like to define a method the following method using Eisbach:
method transfer_prover' = (fold relator_eq; transfer_prover)
Unfortunately, I get an exception at the method declaration time (both with Isabelle2016 and 1e7c5bbea36d):
exception THM 0 raised (line 884 of "thm.ML"):
The problem seems to be the named_theorems "relator_eq" which I am passing to the method "fold", as the following minimal testcase shows
method bar = (fold One_nat_def) (* works *)
method foo = (fold test) (* fails *)
Why can't I use "fold" with named_theorems in Eisbach method definitions?
This archive was generated by a fusion of
Pipermail (Mailman edition) and