[isabelle] Eisbach: fold and named_theorems



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




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