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

Brian Huffman wrote:
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.

sorry - my mistake - I'd only loaded Pure (which was all I'd ever built for Isabelle2009-2)


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