Stream: Beginner Questions

Topic: Help with syntax error.

view this post on Zulip Thomas Gebert (Jul 30 2025 at 19:14):

Hi, I am re-learning how to use Isabelle again to play with the LTL stuff.

I'm afraid that I'm very out of practice with the syntax for Isabelle, so I'm getting errors that I'm not 100% sure how to fix.

I am trying to write this: 

theory SanityCheck
  imports "LTL.LTL"
begin

definition p :: "'a ⇒ bool" where
  "p _ = True"

lemma excluded_middle: "Or_ltlc (LTL.Prop_ltlc p) (LTL.Not_ltlc (LTL.Prop_ltlc p)) ≡ LTL.True_ltlc"
  by sorry

end

and I am getting this error:

Outer syntax error⌂: keyword "(" expected,
but end-of-input⌂ was found

Can someone tell me the correct syntax?

view this post on Zulip terru (Jul 30 2025 at 20:16):

just leave out the by (sorry closes the goal on its own, it's not a proof method that could be applied to by or apply the way simp/auto/etc. are)

view this post on Zulip Thomas Gebert (Jul 30 2025 at 20:28):

Ah, ok, that fixed it. I really need to reread the concrete semantics book. Thanks!

Last updated: Aug 13 2025 at 08:30 UTC