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



Quoting rpollack at inf.ed.ac.uk:

Thanks Makarius,

   by
     (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
   done

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?

Best,
Randy


--
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.