Stream: Beginner Questions

Topic: quotes versus angle brackets

Adam Dingle (Mar 28 2026 at 08:06):

In Isabelle it seems that "x + y" and ‹x + y› are synonymous. For example, I can write

fun conj :: "bool ⇒ bool ⇒ bool" where
  "conj True True = True" |
  "conj _ _ = False"

or

fun conj :: ‹bool ⇒ bool ⇒ bool› where
  ‹conj True True = True› |
  ‹conj _ _ = False›

and Isabelle will happily accept either form.

Why do both of these syntaxes exist? Is one preferred over another in certain situations?

Mathias Fleury (Mar 28 2026 at 08:27):

" is the "older" form

Mathias Fleury (Mar 28 2026 at 08:27):

It is easier to type, but it has a major drawback: you cannot put quotes within quotes

Mathias Fleury (Mar 28 2026 at 08:28):

There is no way to parse:

ML "@{term "x=y"}"

Mathias Fleury (Mar 28 2026 at 08:28):

while ML ‹@{term ‹x=y›}› is clear

Last updated: Apr 14 2026 at 09:21 UTC