Andreas Lochbihler

2016-08-11 07:06:33 UTC

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"):

symmetric

TERM _

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 *)

named_theorems test

declare One_nat_def[test]

method foo = (fold test) (* fails *)

Why can't I use "fold" with named_theorems in Eisbach method definitions?

Best,

Andreas

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"):

symmetric

TERM _

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 *)

named_theorems test

declare One_nat_def[test]

method foo = (fold test) (* fails *)

Why can't I use "fold" with named_theorems in Eisbach method definitions?

Best,

Andreas