[isabelle-dev] ctxt --?--> simplifier
wneuper at ist.tugraz.at
Thu Apr 14 18:47:48 CEST 2011
searching for how Isabelle/Isar handles contexts, for instance, in
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
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