Re: [isabelle] &&, force, inputting facts, again

Quoting rpollack at

Thanks Makarius,

     (insert h[where S="{}"], force,
      insert h[where S ="UNIV::nat set"], force)

This seems the clearest to me.

I was happy too soon. This proof sends both facts to "force" on the second goal, thus is slow. The other proof you suggested

   using h[where S="{}"] apply force
   using h[where S ="UNIV::state set"] apply force

is fast, and does the intended search, but isn't pure Isar. Does Isar have a vernacular form that sends the first fact to the first goal, and only the second fact to the second goal, without restating the second goal?


The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

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