title: Does Isabelle/HOL have its tactic language?
body: <p>Coq has tactic language Ltac with match facilities and so on. Does Isabelle/HOL have some programming language for tactics with the services for parsing, pattern matching and so on? I skimmed through Isabelle's Isar reference manual and the old Pawlson tutorial but I have found cues for that.</p>