[isabelle] where string?



Hi
I would like to apply a rule after replacing (?t::char list) a variable of type string by a string value ' 's' '

When I attempt

apply (rule lkeval.simps(1) [where t = ' 's' '])

I am told

*** Outer lexical error: bad input "' 's' ']); \<^sync> ..."
*** Outer syntax error: keyword "]" expected,
*** but bad input ' 's' ']); was found
*** Outer lexical error: bad input "' 's' ']); \<^sync> ..."

is there a problem replacing variables by string values or have I missed something?

david










This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.