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