Re: [isabelle] where string?



David,

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

The string notation ''s'' is only inner syntax (terms, types) not outer syntax (commands). You must put additional quotes:

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

Alex





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