[isabelle-dev] NEWS: Proof method "use" in Pure
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
(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