[isabelle-dev] ctxt --?--> simplifier

[Lars Noschinski]

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

lemma ctxt:
assumes asm1: "a = 1" and asm2: "b = -2"
shows "2 * a + b = (0::int)"
apply (insert asm1 asm2)
apply simp

instead.

  -- Lars