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

Makarius makarius at sketis.net
Thu Jul 21 12:03:55 CEST 2016

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


More information about the isabelle-dev mailing list