*** 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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to