Re: [isabelle] simpsets



On Wed, 16 Aug 2006, Jeremy Dawson wrote:

> but in a recent development snapshot
> 
> > > simpset () addsimps [refl] addsimps [refl] ;
> val it = ? : MetaSimplifier.simpset
> > simpset () addsimps [refl] ;
> val it = ? : MetaSimplifier.simpset
> > Addsimps [refl] ;
> ### Ignoring duplicate rewrite rule:
> ### ?x1 = ?x1 == True
> val it = () : unit
> 
> What's happening here?

This is due to a recent change in producing the warning messages.  A 
simpset that is explicitly drawn from the context (simpset()) to be used 
in actual simplification acts silently in this respect.


> Does simpset () now return a different simpset from the current default? 
> Should Simp_tac work the same as simp_tac (simpset ()) ?

It should be still the same, but note that both simpset() and the capital 
Simp_tacs are essentially legacy.  Better pass through an explicit 
Proof.context and use local_simpset_of.


	Makarius





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