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

[Walther Neuper]

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 ?

Walther

PS: I assume, that asm1 and asm2 are contained in the context; I am 
interested in which format the simplifier provides asm1 and asm2 to the 
simplifier.