On Mon, 2 Apr 2012, Makarius wrote:
On Mon, 26 Mar 2012, Peter Lammich wrote:
I tried to follow the approach done in the cancellation simprocs,
getting something like:
fun assn_simproc_fun ss credex = let
val ctxt = Simplifier.the_context ss
val ([redex],ctxt') = Variable.import_terms true [term_of credex]
ctxt;
val result = Option.map (export o mk_meta_eq)
(Arith_Data.prove_conv_nohyps
[simp_tac (HOL_basic_ss addsimps @{thms star_aci}) 1] ctxt
(redex,new_form)
);
Another fine point: redex lives in ctxt' so you should normally pass that
to tools operating on it.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
