Fair enough :) FWIW the differences are largely syntactic. Some of them are due to implication or quantification being in the meta-level (Pure, Λ/long ⇒) vs ob

Fair enough :) FWIW the differences are largely syntactic. Some of them are due to implication or quantification being in the meta-level (Pure, Λ/long ⇒) vs object-level (HOL, ∀/⟶). Transporting between them (for HOL) is easy and the automation tends to normalize object-level quantification and implication into meta-level. "assume P show Q" is just Isar-syntax for a structured proof of "P ==> Q" (which is a term).