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


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