Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] where string?

view this post on Zulip Email Gateway (Aug 18 2022 at 11:34):

From: Alexander Krauss <krauss@in.tum.de>
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

Last updated: Jan 04 2025 at 20:18 UTC