[isabelle] adding a looper to the simplifier
-----BEGIN PGP SIGNED MESSAGE-----
Dear Isabelle users,
I am trying to add a looper to the simplifier to do some "risky"
simplifications that I cannot do with the splitter. I am stuck, because
the simplifier loops, and I do not understand why. Here is what I do:
val my_ss = HOL_basic_ss;
(* At this place, I later intend to add some interesting simplification
procedures to my_ss. *)
(* Register a new looper *)
(fn ss => ss addloop ("foo", Simplifier.simp_tac my_ss));
On the last command, the simplifier loops. According to the trace it is
invoked again and again on "False". I would expect the simplifier to
fail on "False", because my newly added looper fails on "False".
Any explanations / comments / pointers are very welcome!
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org
-----END PGP SIGNATURE-----
This archive was generated by a fusion of
Pipermail (Mailman edition) and