[isabelle] simpsets




In Isabelle 2005,

> simpset () addsimps [refl] ;
### Ignoring duplicate rewrite rule:
### ?x1 = ?x1 == True
val it = ? : FullMetaSimplifier.simpset
> Addsimps [refl] ;
### Ignoring duplicate rewrite rule:
### ?x1 = ?x1 == True
val it = () : unit

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? Does simpset () now return a different simpset from the current default?
Should Simp_tac work the same as simp_tac (simpset ()) ?
(as I always understood it did, but I'd like to know whether it still does, since I'm trying to debug a proof which doesn't seem to use the simplification rules I'm expecting it to)

Thanks,

Jeremy





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