Adam Dingle (Mar 15 2026 at 10:23): Adam Dingle (Mar 15 2026 at 10:23):Pure/Examples/Higher_Order_Logic.thy defines implication like this:
axiomatization imp :: "o ⇒ o ⇒ o" (infixr ‹⟶› 25)
But in HOL/HOL.thy it looks a bit different:
axiomatization implies :: "[bool, bool] ⇒ bool" (infixr ‹⟶› 25)
I don't understand the meaning of [bool, bool] here. The grammar in section 8.4.3 "The Pure grammar" of the Isabelle reference indicates that a type may have the form [type, ..., type], but doesn't explain it at all. Any pointers?
Mathias Fleury (Mar 15 2026 at 13:01):the bracket notation is the same as an arrow
Mathias Fleury (Mar 15 2026 at 13:01):it exists both for types and terms
Mathias Fleury (Mar 15 2026 at 13:04):(Terms use [[ ... ]] )
Adam Dingle (Mar 15 2026 at 14:07):Aha, thanks. If this notation has the same meaning, why does it exist? Because someone thinks it looks nicer? Also, is this documented somewhere?
Mathias Fleury (Mar 15 2026 at 14:25):You can here https://stackoverflow.com/questions/15939265/how-do-i-display-brackets-around-assumptions-in-isabelle-jedit how to activate it.
Mathias Fleury (Mar 15 2026 at 14:25):Some people like it more
Last updated: Mar 25 2026 at 02:29 UTC