There are meta symbols for implication and universal quantification in Isabelle/Pure (⟹ and ⋀), which behave differently from its HOL counterparts (∀ and →).
Is there a meta symbol for existential quantification? If not, is there a specific reason for this decision?
Pure is based on intuistionistic logic and there is no existential quantifier in this logic.
The rough equivalent is obtains:
lemma
assumes "P"
obtains x where "Q x"
The generated lemma is P ⟹ (⋀x. Q x ⟹ thesis) ⟹ thesis. It does not contain an existential quantifier, but only an implication. However it plays a similar rule: by instantiation of thesis with any other goal, you can exhibit the existence of an x such that Q x.