*** 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
*** General ***
* Pure provides basic versions of proof methods "simp" and "simp_all"
that only know about meta-equality (==). Potential INCOMPATIBILITY in
theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order
is relevant to avoid confusion of Pure.simp vs. HOL.simp.
This
See also
http://isabelle.in.tum.de/repos/isabelle/file/2803d2b8f85d/Admin/PLATFORMS#l33
Former Ubuntu 10.04 LTS has become a bit old, and is no longer
maintained by Canonical. 12.04 remains officially active until 04/2017.
The Mac OS X baseline is still 10.8 (Mountain Lion), which is also from
*** Prover IDE -- Isabelle/Scala/jEdit ***
* Completion templates for commands involving "begin ... end" blocks,
e.g. 'context', 'notepad'.
This refers to Isabelle/0f39f59317c1. It can be seen as part of the
standardized indenation policy, although only line breaks without extra
indentation are
