[isabelle] A quick question about fixing variables in a proof
I'm trying to just fix a functional variable in a proof as follows:
G :: "S * T => real"
s :: T
f :: T
locale A =
fixes p :: Obj
assumes cons: "!! t1 t2. G(p,t1) = G(p,t2)"
locale B =
assumes "A p"
interpret localA: A p
interpret localB: B p
have "func(p,s) = func(p,f)"
Does anyone know how to unify 'func' to G and s/f to the second argument?
Why can't auto unify them?
Any help will be much appreciated.
This archive was generated by a fusion of
Pipermail (Mailman edition) and