Let me try to explain the difference from the perspective of a user. There are
three classical tools that will behave differently: safe, clarify and clarsimp.
Each of these will, when it would have substituted and removed equalities in
the past, now substitute those equalities, possibly reorient
This sounds logical. But what about auto? Like the other three, it is used to
perform obvious steps in a proof, and it is not terminal.
Larry
On 1 Sep 2010, at 14:17, Thomas Sewell wrote:
> Let me try to explain the difference from the perspective of a user. There
> are three classical tools th
For some week or so there are sparadic failures of HOL-Decision_Procs like
this:
HOL-Decision_Procs FAILED
(see also
/Users/makarius/.isabelle/heaps//polyml-5.4.0_x86_64-darwin/log/HOL-Decision_Procs)
(Var 0))
(replicate 3 None) [0, 0, 0]
approx_tse_form 30 3 1
(Bound (Var 0) (
I always intended auto to be initial rather than terminal. I'm not aware of the
unsafe mode you refer to, but it may have been introduced later.
Larry
On 1 Sep 2010, at 14:40, Thomas Sewell wrote:
> Good point - I think of auto as terminal. My understanding was that auto had
> both a safe and u
Am Mittwoch, den 01.09.2010, 15:40 +0200 schrieb Makarius:
> For some week or so there are sparadic failures of HOL-Decision_Procs like
> this:
[..]
> This only happenes when running in parallel mode, which is the default
> on modern hardware for quite some time already. I estimate the
> probabi
On Wed, 1 Sep 2010, Johannes Hölzl wrote:
The Approximation theory only uses relfection and the code generator
(with setup for code integer and efficient nat). Last year the usage of
Unsynchronized.ref was remove in reflection. Since this time the
approximation method should not use any referenc
