[isabelle-dev] NEWS: method facts

*** Isar *** * Proof methods may refer to the main facts via the dynamic fact "method_facts". This is particularly useful for Eisbach method definitions. * Eisbach provides method "use" to modify the main facts of a given method expression, e.g. (use facts in simp) (use facts in ‹simp add:

Re: [isabelle-dev] Whole word search

On 07/06/16 10:10, Fabian Immler wrote: > >> Am 06.06.2016 um 21:29 schrieb Makarius : >> >> It means that the parts of long identifiers can be selected individually >> (e.g. via double-clicked). It also has an effect on searching "x" in >> "x.", but note that the lambda in