[isabelle-dev] NEWS: Proof method "use" in Pure

[Makarius]

*** Isar ***

* Proof method "use" allows to modify the main facts of a given method
expression, e.g.

  (use facts in simp)
  (use facts in ‹simp add: ...›)


This refers to Isabelle/59eff6e56d81. Before, the proof method "use" was
part of Eisbach, which is still not in Pure because of its workarounds
for attributes "of" and "where" that still need to be re-unified.

The method "use" might turn out useful to eliminate method "insert" in
many situations, as well as rule_tac etc. where a particular flow of
facts is required.


	Makarius