On Fri, 22 Jul 2011, Lars Noschinski wrote:
In this case it also works for the simplifier. Actually, I had to go to the
old HOL manual, to find out, why one would usually use the splitter for this.
In our case, the if is in the assumption, so one would need
(simp split: split_if_asm)
here instead. But I'm quite fuzzy on the semantics of the split
parameter -- why would split_if be applied to the conclusion and
split_if_asm to the hypotheses? Is there somewhere a high-level
description of the splitter?
These ancient explanations of simplifier components are still awaiting to
be updated and moved to isar-ref. I have recently done most of that for
the classical reasoner, in conjunction with some "localization" and
simplification of the implementation (except for wrappers and addss stuff,
which is seen in Isar source as "fastsimp").
I will continue that eventually.
BTW: Is the isar-ref documentation about the split method correct? It
does not seem (and need) to accept the "(asm)" option?
That is indeed a bit outdated -- more than 10 years. See now
http://isabelle.in.tum.de/repos/isabelle/rev/f7bbfdf4b4a7
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
