[isabelle-dev] ctxt --?--> simplifier
noschinl at in.tum.de
Fri Apr 15 10:47:21 CEST 2011
On 14.04.2011 18:47, Walther Neuper wrote:
> searching for how Isabelle/Isar handles contexts, for instance, in
> lemma ctxt:
> assumes asm1: "a = 1" and asm2: "b = -2"
> shows "2 * a + b = (0::int)"
> using asm1 asm2 by (simp)
> I got stuck in reading the code somewhere at Expression.read_statement
> and Element.activate.
> Who quickly has a precise pointer into the code ?
As you can see in Simplifier.method_setup, Method.insert_tac is called
to insert the chained facts into the goal, before calling the simplifier.
On the Isar level, you can see what happens by using
assumes asm1: "a = 1" and asm2: "b = -2"
shows "2 * a + b = (0::int)"
apply (insert asm1 asm2)
More information about the isabelle-dev