How to type boldface symbols in Isabelle

The definition of semigroup and monoid uses bold * and bold 1


locale semigroup =
  fixes f :: "'a ⇒ 'a ⇒ 'a"  (infixl "❙*" 70)
  assumes assoc [ac_simps]: "a ❙* b ❙* c = a ❙* (b ❙* c)"


locale monoid = semigroup +
  fixes z :: 'a ("❙1")
  assumes left_neutral [simp]: "❙1 ❙* a = a"
  assumes right_neutral [simp]: "a ❙* ❙1 = a"

(They don't print well outside of jEdit and instead there is the ❙ symbol)

How do I type those symbols in jEdit? Or more generally, is there some way to lookup ASCII version of any symbol in jEdit?

Solution

You need to type \<^bold> (usually just typing \b is enough for autosuggestion to pop up). This will give you the bar ❙. Any symbol you place after the bar will become bold.