Re: [isabelle] [isabelle-dev] Rewriting wrt other axioms

On Wed, Feb 16, 2011 at 4:57 AM, Jeremy Dawson
<jlcaadawson at> wrote:
> Unfortunately HOL_basic_ss doesn't seem to exist anymore. You could try
> empty_ss instead (I've never used it myself). (see s9.2.2)

HOL_basic_ss still exists! I am using it all over the place in the
implementation of the HOLCF domain package, and a quick grep of the
current sources shows that it is used in plenty of other places too.

> Or try rewrite_rule [a2] a1 (see s4.1.3 of the Reference Manual)

I believe that Meta_Simplifier.rewrite_rule corresponds precisely to
the "unfolded" attribute, which is similar to "simplified", except
that it uses a more basic kind of rewriting (no pre-processing of
rules, no using local assumptions, no congruence rules, etc.)

- Brian

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.