Andrea Vezzosi (May 31 2023 at 12:29): Andrea Vezzosi (May 31 2023 at 12:29):I get an inner syntax error at "5.5" with the following lemma declaration:
lemma step1b: "11 = 2 * 5.5"
What could be the problem? I have used decimal points elsewhere and it's been fine.
Mathias Fleury (May 31 2023 at 12:40):Forgot to import Complex_Main?
Andrea Vezzosi (May 31 2023 at 12:59):yep, that was it, thanks!
Wolfgang Jeltsch (May 31 2023 at 17:32):Importing HOL.Real should be enough. Or is it with Complex_Main like with Main: import this theory instead of ancestor theories of it?
Mathias Fleury (Jun 01 2023 at 05:02):from my understanding Complex_Main and Main and starting points and you should import them instead of anything from HOL
Wolfgang Jeltsch (Jun 01 2023 at 11:42):Mathias Fleury said:
from my understanding
Complex_MainandMainand starting points and you should import them instead of anything fromHOL
Okay, good to know.
How is it actually with theories from sessions other than HOL. Which of these can be expected to directly or indirectly import Main, so that an explicit import of Main is not necessary? I think that at least HOL-Eisbach.Eisbach does not import Main: I had trouble in the past when importing it before Main.
Manuel Eberl (Jun 06 2023 at 12:24):Do note also that you typically want to add a type constraint with statements such as these, e.g. 11 = 2 * (5.5 :: real). Otherwise Isabelle infers a very general type, which is usually not what you want.
Wolfgang Jeltsch (Jun 06 2023 at 22:54):Yes, @Andrea Vezzosi and I already discovered that. :smile:
Last updated: Nov 13 2025 at 04:27 UTC