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

Walther Neuper wneuper at ist.tugraz.at
Thu Apr 14 18:47:48 CEST 2011

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 ?


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 

More information about the isabelle-dev mailing list