I'm using Isabelle/HOL. Isabelle exports the last fact in a block, allowing the context that contains the block to use it. Ordinarily when I generate facts, I can give them convenient names. How do I name facts that are exported from blocks?
lemma mylemma: "i=i"
have "j=j" by auto
show ?thesis using ‹⋀j. j = j› by auto
Right now I use
‹⋀j. j = j› to refer to the exported fact as a proposition literal. I'd like to be able give it a simple name, though, as when I named the lemma
mylemma. Thanks for any suggestions!