Re: [isabelle] assumptions format in isar



Hi Julien,

a neat way is the empty proof-method "-". It only has the effect of inserting 
the chained facts to the goal:

...
ultimately have main
  apply -
  apply ...

Since the by command accepts an initial and an final method the following  
pattern may also occur:

ultimately have main
  by - (...)


   Norbert





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